PLC Program Translation for Verification Purposes

CímPLC Program Translation for Verification Purposes
Közlemény típusaJournal Article
Kiadás éve2017
SzerzőkDarvas, D., Majzik, I., and Blanco Viñuela, E.
FolyóiratPeriodica Polytechnica, Electrical Engineering and Computer Science
Kiadás dátuma05/2017
Kulcsszavakformal verification, PLC, programming languages, semantics
Programmable logic controllers are typically programmed in one of the five languages defined in the IEC 61131 standard. While the ability to choose the appropriate language for each program unit may be an advantage for the developers, it poses a serious challenge to verification methods. In this paper we analyse and compare these languages to show that the ST programming language can efficiently and conveniently represent all PLC languages for formal verification purposes. Furthermore, we provide a translation method from IL to ST programming languages (for the Siemens implementation), together with a sketch of proof for its correctness. This allows the usage of the ST-based PLCverif model checking method for safety PLC programs.
Refereed DesignationRefereed