Automatically Deriving Symbolic Invariants for PLC Programs Written in IL - Forms/Format 2010 - page 237

Automatically Deriving Symbolic Invariants for
PLC Programs Written in IL

Sebastian Biallas 1 ,JörgBrauer 1 , Stefan Kowalewski 1 , and Bastian Schlich 2

1 Embedded Software Laboratory, RWTH Aachen University
{biallas, brauer, kowalewski}@embedded.rwth-aachen.de
2 Industrial Software Systems, ABB Corporate Research
[e-mail]

Abstract. In this paper, we propose a new approach to automati-
callyderiveinvariantsfromProgrammableLogicControllerprograms
by symbolically rewriting Instruction List code. These invariants de-
scribe the relations between all variables and capture the behavior
of the program. Usually, invariants are created by users and ver-
ified 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 tech-
niques to verify them. Users only need to inspect the generated in-
variants and compare them to the expected program behavior. Using
three example programs of different sizes, we show that the gener-
ated invariants are easy to understand and that the approach indeed
scales for larger programs.

Keywords: Program Verification, Invariants, PLC, Instruction List

1 Introduction

Programmable Logic Controllers (PLCs) are frequently used in safety-critical
systems, where the application of formal verification methods is recommen-
ded [10]. In the past, formal methods such as model checking [17,15] or static
analysis [8] have been applied to this task. Model checking, for instance, is
used to verify whether the model of a systems satisfies the system's require-
ments. The generation of the model can in many cases be done automatically.
However, expressing requirements, which are often given in natural language,
in terms of temporal logic, is a very time-consuming and error-prone process.
Despite the advances in this regard [12], this drawback limits the appli-
cability of formal verification methods to industrial applications. To alleviate

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), Ger-
man Research Foundation grant DFG EXC 89.