Currently, PLCs are increasingly being used to implement safety function for safety critical systems. One of the preferred languages in this area is FBD (Function Block Diagram) according to IEC 61131-3. There are many research projects in the verification and implementation field of function block libraries according to this standard. However safety issues are not addressed in IEC 61131-3 and PLC programming software packages have only library function blocks dealing in general with communication, mathematical operations, logic and so on. As step for building safety application in IEC 61131-3 FBD according to IEC 61508, PLCopen specifies a set of called SFBs (Safety Function Blocks). Several manufacturers of IEC 61131-3 programming tools have already implemented libraries according to this specification.
The main goal of the presented work is to ease the verification of safety application built up using the PLCopen SFBs in one of the commercially available tools. To this end a modular of function block oriented approach is taken. For all specified SFBs a corresponding formal model is built using TA (Timed Automata). The formal model of the application is derived by combining the previously specified TA in the same structure as the original SFBs are combined in the PLC software to verify a safety application.
Before application can be verified, it has to be assured that the formal models are actually describing the behavior of the SFBs correctly. The description of SFBs by PLCopen consists three parts for each SFB respectively:
1. The internal states graphical description and behavior using a state diagram.
2. A properties list described in natural language.
3. Timing diagrams describing the temporal behavior for some specific scenarios.
In the presented approach the graphical description is translated into a TA in the language of the Upload tool. Simulations of the model are performed and the results are compared to the timing diagrams to validate the temporal behavior.
Constructing the Safety Function Block Library
Uppaal allows analysis of networks of timed automata with binary synchronization. It consists three main parts. First, timed processes are described using a graphical editor. Second, systems can be simulated by a graphical simulator. Third, reach ability properties can be verified using the verifier.
The process depicted is followed to formalize an SFB. First of all the input or output variables of the SFB are declared according to the interface description in the PLCopen document. Next, the state diagram is transferred to TA using the graphical editor of Upaal. Depending on the TA and the input sequence scenario extracted from the timing diagram, a simulation is executed to validate the temporal behavior using the graphical simulator. Thereafter, the textual properties are translated into TL (Temporal Logic) formula. The properties of the safety function can be verified using the verifier. The use of symbolic model actually checking in combination with TA would be sufficient to verify the behavior of the formalized SFBs. However, the additional use of simulation is useful for two distinct reasons. First all to validate specific scenarios presented in the specification it is the more direct approach. Second, and much more important, it allows users not familiar with formal models to assess the results directly. All twenty SFBs defined by PLCopen have been formalized according to this procedure in the frame of the presented work.
A Textual Functional description of the SFB is as follows: this function block convert two equivalent SAFEBOOL inputs to one SAFEBOOL output with discrepancy time monitoring. Both input Channel A and B are interdependent. The function block output shows the result of the evaluation of both channels. If one channel signal changes from TRUE to FALSE the output switches off immediately for safety reasons.
The inputs are used as transition guards and the outputs are updated according to the state location. The input of time is assumed as a clock.