Verification and validation of safety applications based on PLCopen safety function blocks

Functional Safety is a major concern in the design of automation systems today. Many of those systems are realized using Programmable Logic Controllers (PLCs) programmed according to IEC 61131-3. PLCopen – as IEC 61131 user organization – semi-formally specified a set of software function blocks to be used in safety applications according to IEC 61508. In the presented work, formal models in the form of timed automata for the safety function blocks (SFBs) are constructed from the semi-formal specifications. The accordance of the formalized blocks to the specification is verified using model checking. Furthermore, their behaviour is validated against specified test cases by simulation. The resulting verified and validated library of formal models is used to build a formal model of a given safety application – built from SFBs – and to verify and validate its properties.

Research highlights
► Formalization of the PLCopen specification of safety function blocks (SFBs).
► Transformation of SFBs into timed automata.
► Verification and validation of single SFBs using the UPPAAL model checking tool.
► Translation of PLC programs built from SFBs into sets of communicating automata.
► Verification and validation of PLC programs in UPPAAL using an illustrative example.