PLC programs' checking method and strategy based on module state transfer

PLC (Programmable Logic Controller) program in automatic control is vital to this kind of safety-critical applications. In this paper, we present a useful method of compositional model checking for verification of PLC programs. The method is based on the work pattern and the system model of PLC for modelling PLC program. Because the state space explosion problem limits the use of general model checking in real PLC programs, the paper firstly defines the framework and the mechanism of model combination based on the module of PLC program. Then the paper proposes a series of PLC domain specific strategies for compositional model checking between two modules. Through two modules' combination is verified at a time in a PLC program, cyclic stacking combination of the modules can be verified by the recursive operation of compositional checking for the whole program. The strategies can effectively reduce state space by means of hierarchical module model and recursion state transfer. The validity of our method is illustrated by an example.