ABSTRACT
Programmable Logic Controllers (PLC) play a fundamental role in Industrial Control Systems, as they provide various functionalities of physical tools by collecting data from input devices and sending commands to output devices. In this paper, we introduce a formal framework for software verification of the robustness of PLC programs. In particular, (i) we identify external vulnerabilities based on dynamic Internet of Things (IoT) interactions; (ii) we define the semantics of Structured Control Language (SCL) and the semantics of Timed Automata, (iii) we provide a set of transformation rules to transform a program written in SCL to a Timed Automaton and (iv) we show their correctness with respect to the corresponding semantics. Finally, we apply Model Checking tools to verify robustness properties of the PLC source code.
