Software Verification of PLC programs

Programmable Logic Controllers (PLC) play an important role in Industrial Control Systems, as they manage the actions of physical tools by collecting data from input devices and sending commands to output devices. In this thesis, we introduce a formal framework for software verification of robustness of PLC programs. In particular, we identify external vulnerabilities based on dynamic user interaction, we define the semantics of Structured Control Language (SCL) and the semantics of Timed Automata (TA), we provide a set of transformation rules to transform a program written in SCL to a Timed Automaton, and we show their correctness with respect to the corresponding semantics. By applying these transformation rules, we can apply Model Checking tools (namely UPPAAL) to verify robustness properties of the PLC source code.