Regression Verification for Programmable Logic Controller Software
Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, and Alexander Weigl
Automated production systems are usually driven by Programmable Logic
Controllers (PLCs). These systems are long-living - yet have to adapt to
changing requirements over time. This paper presents a novel method for
regression verification of PLC code, which allows one to prove that a new
revision of the plant's software does not break existing intended behavior.
Our main contribution is the design, implementation, and evaluation of a
regression verification method for PLC code. We also clarify and dene the
notion of program equivalence for reactive PLC code. Core elements of our
method are a translation of PLC code into the SMV input language for model
checkers, the adaptation of the coupling invariants concept to reactive
systems, and the implementation of a toolchain using a model checker
supporting invariant generation.
We have successfully evaluated our approach using the Pick-and-Place Unit
benchmark case study.