@article {6134,
	title = {PLC Program Translation for Verification Purposes},
	journal = {Periodica Polytechnica, Electrical Engineering and Computer Science},
	volume = {61},
	year = {2017},
	month = {05/2017},
	pages = {151{\textendash}165},
	abstract = {<div>
	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.</div>
},
	keywords = {formal verification, PLC, programming languages, semantics},
	issn = {2064-5279},
	doi = {10.3311/PPee.9743},
	author = {D{\'a}niel Darvas and Istv{\'a}n Majzik and Blanco Vi{\~n}uela, Enrique}
}
