Combinational model-checking of PLC programs´ verification based on instructions

The correctness of 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 combinational model-checking for correctness of PLC programs. The method is based on the denotational semantics of PLC program and the semantic functions for basic instructions. Because the state space explosion problem limits the use of general model-checking in real PLC programs, the paper firstly defines a set of combinational verification rules based on the denotational semantics. Then the paper proposes a series of general and PLC domain specific strategies for combinational model-checking. The rules and strategies can effectively reduce state space and their correctness is proved. The validity of our method is shown by an example.