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.
formal verification function blocks iec 61131-3 tabular expressions critical systems