PLC Program Translation for Verification Purposes
Cím | PLC Program Translation for Verification Purposes |
Közlemény típusa | Journal Article |
Kiadás éve | 2017 |
Szerzők | Darvas, D., Majzik, I., and Blanco Viñuela, E. |
Folyóirat | Periodica Polytechnica, Electrical Engineering and Computer Science |
Kötet | 61 |
Kiadás | 2 |
Pagination | 151–165 |
Kiadás dátuma | 05/2017 |
ISSN | 2064-5279 |
Kulcsszavak | formal verification, PLC, programming languages, semantics |
Összefoglalás |
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.
|
DOI | 10.3311/PPee.9743 |
Refereed Designation | Refereed |