Translation-Based Model Checking for PLC Programs

In this paper, we focus on modeling and verification of PLC systems, which are widespread in industry and manufacture. Our approach is based on a translation procedure from PLC programs to timed automata. The resulting model consists of several kinds of modules. Besides the main module which depicts the behaviors of the PLC programs, a dedicated module is constructed to simulate the cyclical running mode of PLC systems, and another module is involved for specifying the environment behaviors. After all modules are constructed, the model checker Uppaal is adapted to perform the model checking. Experimental results show promising performance of our approach. Compared with existing approaches, our method supports extensive instructions, including not only the time-related instructions, such as timer and counter, but also the subroutine and interruption instructions. In addition, the structure of whole model is more compact, and the translation procedure is more efficient, which results in a reduced verification model.