PLC Modeling and Checking Based on Formal Method

Yueshan Zheng, Guiming Luo, Junbo Sun, Junjie Zhang, Zhenfeng Wang

.

DOI: 10.4236/jsea.2010.311124                

Abstract

High reliability is the key to performance of electrical control equipment. PLC combines computer technology, automatic control technology and communication technology and becomes widely used for automation of industrial processes. Some requirements of complex PLC systems cannot be satisfied by the traditional verification methods. In this paper, an efficient method for the PLC systems modeling and verification is proposed. To ensure the high-speed property of PLC, we proposed a technique of “Time interval model” and “notice-waiting”. It could reduce the state space and make it possible to verify some complex PLC systems. Also, the conversion from the built PLC model to the Promela language is obtained and a tool PLC-Checker for modeling and checking PLC systems are designed. Using PLC-Checker to check a classical PLC example, a counter-example is found. Although the probability of this logic error occurs very small, it could result in system crash fatally.

Keywords

Model Checking, PLC Modeling, PLC-Checker, Formal Method

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	Pavlovic, R. Pinger and M. Kollmann, “Automated Formal Verification of PLC Programs Written in IL,” Conference on Automated Deduction (CADE), Bremen, July 2007, pp. 152-163.
[2]	M. B. Younis and G. Frey, “Formalization of Existing PLC Programs: A Survey,” Proceedings of CESA 2003, Lille, 2003.
[3]	N. Bauer, S. Engell, S. Lohmann, M. Remelhe and O. Stursberg, “Verification of PLC Program Given as Sequential Function Charts,” Lecture Notes in Computer Science, Vol. 3147, 2004, pp. 517-540.
[4]	S. R. Koo, P. H. Seong and S. D. Chaa, “Software Design Specification and Analysis Technique for the Safety Critical Software based on Programmable Logic Controller (PLC),” Proceedings of the Eighth IEEE International Symposium on High Assurance Systems Engineering (HASE’04), Florida, March 2004, pp. 283-284.
[5]	A. Mader and H. Wupper, “Timed Automaton Models for Simple Programmable Logic Controllers,” Proceedings of the 11th Euromicro Conference on Real-Time Systems 1999, York, June 1999, pp.106-113.
[6]	E. Brinksma1, A. Mader and A. Fehnker, “Verification and Optimization of a PLC Control Schedule,” International Journal on Software Tools for Technology Transfer (STTT), Vol. 4, No. 1, October 2002, pp. 21-33.
[7]	S. Lamp′eri`ere and J. J. Lesage, “Formal Verification of the Sequential Part of PLC Programs,” 5th Workshop on Discrete Event Systems (WODES 2000), Ghent, August 2000, pp. 247-254.
[8]	S. Kowalewski, S. Engell, J. Preu?ig and O. Stursberg, “Verification of Logic Controllers for Continuous Plants Using Timed Condition/Event-System Models,” Automatica: Special Issue on Hybrid Systems, Vol. 35, No. 3, March 1999, pp. 505-518.