Safety Verification of IEC 61131-3 Structured Text Programs

With the development of the industrial control system, programmable logic controllers (PLCs) are increasingly adopted in the process automation. Moreover, many PLCs play key roles in safety-critical systems, such as nuclear power plants, where robust and reliable control programs are required. To ensure the quality of programs, testing and verification methods are necessary. In this article, we present a novel methodology which applies model checking to verifying PLC programs. Specifically, we focus on the structured text (ST) language which is a widely used, high-level programming language defined in the electro-technical commission (IEC) 61131-3 standard. A formal model named behavior model (BM) is defined to specify the behavior of ST programs. An algorithm based on variable state analysis for automatically extracting the BM from an ST program is given. An algorithm based on the automata-theoretic approach is proposed to verify linear temporal logic properties on the BM. Finally, a real-life case study is presented.