Logo Universität Bremen


Universität Bremen - Fachbereich 3 - Informatik


Startseite Detail

Counterexample-Guided Abstraction Refinement for PLCs

Datum: 15.11.2011
Uhrzeit: 17 Uhr c.t.

Ort: Cartesium Rotunde

Vortragende(r): Dipl.-Inf. Jörg Brauer (RWTH Aachen)


Programmable logic controllers (PLCs) are often used to control
safety-critical systems, for which formal verification is desirable,
if not recommended. Model checking is one particular technique
to prove correctness of software written for PLCs. The execution
of programs on PLCs follows the so-called cyclic scanning mode,
which consists of sensing inputs, processing data, and writing
outputs. Each of these steps is executed atomically. A model
checker then has to simulate the execution cycle for all possible
combinations of input values. Since outputs become visible only
at the end of a cycle, internal states within a cycle are not
relevant to verification of input-output relations.

To efficiently verify software for PLCs, we present a method for model
checking programs written in Instruction List (IL) using the
counterexample-guided abstraction refinement (CEGAR) approach.
Using this technique, an initial (coarse) abstraction is iteratively
during the model checking process until either a legitimate counterexample
is found or the software is proved correct. Our technique is tailored to
PLCs by accounting for the cyclic scanning mode. In particular, the
hardware model poses the need for on-the-fly abstraction
refinement. It also allows to treat refinement phases triggered by input
and global variables differently, leading to a more efficient
The effectiveness of this approach is shown in a case study, which
highlights the verification process for function blocks that implement a
specification provided by the industrial consortium PLCopen.