Formal verification of function blocks applied to IEC 61131-3

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.