Proving Equivalence between Control Software Variants for Programmable Logic
Controllers:
Using Regression Verification to Reduce Unneeded Variant Diversity
Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Bernhard Beckert, and
Birgit Vogel-Heuser
Automated production systems are usually driven by Programmable Logic
Controllers (PLCs). These systems are long-living and have high requirements
for software quality to avoid downtimes, damaged product and harm to
personnel. While commissioning multiple systems of similar type, pragmatic
adjustments of the software are often necessary, which results in two or more
similar variants of initially identical software. For further evolution of the
software, an equivalence analysis of the software’s behavior is beneficial to
merge divergent development branches into a single program version. This paper
presents a novel method for regression verification of PLC code, which allows
one to prove that two variants of a plant's software behave identically in
specified situations, despite being implemented differently. For this, a
regression verification method for PLC code was designed, implemented and
evaluated. The notion of program equivalence for reactive PLC code is
clarified and defined. Core elements of the method are the 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. The approach was successfully evaluated
using the Pick-and- Place Unit benchmark case study.