Formal verification of function blocks applied to IEC 61131-3

• We use tabular expressions to formalize requirements of IEC 61131-3 function blocks.
• We use PVS to formalize structured text and FB diagram implementations in IEC 61131-3.
• We formally verify the consistency and correctness for all FBs in IEC 61131-3.
• Using our approach, numerous issues are found in IEC 61131-3 and solutions are suggested.

Many industrial control systems use programmable logic controllers (PLCs) since they provide a highly reliable, off-the-shelf hardware platform. On the programming side, function blocks (FBs) are reusable components provided by the PLC supplier that can be combined to implement the required system behaviour. A higher quality system may be realized if the FBs are pre-certified to be compliant with an international standard such as IEC 61131-3. We present an approach: 1) to create complete and unambiguous FB requirements using tabular expressions; and 2) to verify the consistency and correctness of FB implementations in the PVS proof environment. We apply our approach to the examples in the informative Appendix F of the IEC 61131-3 standard. We examined the entire library of FBs and their supplied implementations described in structured text (ST) and function block diagrams (FBDs). Our approach identified issues in the informative examples, including: a) ambiguous behavioural descriptions; b) missing assumptions; and c) inconsistent implementations. We also proposed solutions to these issues.