Model-based verification of PLC programs using Simulink design

摘要

Programmable Logic Controllers (PLCs) have been widely applied in safety-critical industrial processes. Automated verification of PLC programs is a challenging task for control system engineers. A method of mutation-based verification of Simulink design models for verifying PLCs programs is proposed. In this work, PLC programs coded in the Structured Text (ST) language are assumed to be automatically generated from Simulink models using the tool Simulink PLC Coder from Mathworks. We utilize Simulink diagrams as system design models. Simulink is a powerful design tool for developing complex event-driven applications. To formally verify the functional properties of the design models, a verifying model compiler called Gene-auto is applied to automatically translate Simulink models to C code. The properties to be checked are also translated as C assertions, which are inserted into the translated C code. Then, the generated C code instrumented with assertions is formally verified with a bounded model checking tool for C program called CBMC. The approach is experimentally assessed on a water control system case study. Compared with the previous approach of translating a PLC program to a timed automata and verifying by the use of a model-checking tool, our approach is significantly more scalable to verify non-timing related functional properties.