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.

has been cited by the following article:

• TITLE: PLC Modeling and Checking Based on Formal Method

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

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

  JOURNAL NAME: Journal of Software Engineering and Applications, Vol.3 No.11, November 29, 2010

  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.