Automatically Deriving Symbolic Invariants for PLC Programs Written in IL
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.
Sebastian Biallas, Jörg Brauer, Stefan Kowalewski and Bastian Schlich