Automatically Deriving Symbolic Invariants for PLC Programs Written in IL^★

Abstract

In this paper, we propose a new approach to automatically derive invariants from Programmable Logic Controller programs by symbolically rewriting Instruction List code. These invariants describe the relations between all variables and capture the behavior of the program. Usually, invariants are created by users and verified using formal verification techniques such as model checking or static analysis. The process of manually deriving invariants, however, is error-prone and lengthy. Our approach generates these invariants automatically and removes the need to use formal verification techniques to verify them. Users only need to inspect the generated invariants and compare them to the expected program behavior. Using three example programs of different sizes, we show that the generated invariants are easy to understand and that the approach indeed scales for larger programs.

^★ The work of Sebastian Biallas was supported by the DFG. The work of Jörg Brauer and Stefan Kowalewski was, in part, supported by the DFG Cluster of Excellence on Ultra-high Speed Information and Communication (UMIC), German Research Foundation grant DFG EXC 89.