Paper Info
Title
Plc Programs' Checking Method And Strategy Based On Module State Transfer
Abstract
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.
Year
Venue
Keywords
2015
2015 IEEE INTERNATIONAL CONFERENCE ON INFORMATION AND AUTOMATION
PLC Program, System Model, Compositional Checking, Checking Mechanism, Verification Strategy
Field
DocType
Citations 
Abstraction model checking,Model checking,Computer science,Automatic control,Control engineering,Programmable logic controller,State space,System model,Recursion,Semantics
Conference
0
PageRank 
References 
Authors
0.34
10
4
Name
Order
Citations
PageRank
litian xiao100.34
Li Mengyuan2289.37
Ming Gu355474.82
Jia-guang Sun41807134.30