Regression Verification for Programmable Logic Controller Software

Abstract

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 define 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.

BibTeX

@InProceedings{BeckertUlbrichEA2015,
  author    = {Bernhard Beckert and Mattias Ulbrich and Birgit Vogel-Heuser and Alexander Weigl},
  title     = {Regression Verification for Programmable Logic Controller Software},
  booktitle = {17th International Conference on Formal Engineering Methods (ICFEM 2015)},
  month     = nov,
  year      = {2015},
  keywords  = {IMPROVE},
  url       = {/improve/plc/},
  pages     = {234--251},
  volume    = {9407},
  series    = {LNCS},
  publisher = {Springer},
  doi       = {10.1007/978-3-319-25423-4_15}
}