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.
CITATION STYLE
Beckert, B., Ulbrich, M., Vogel-Heuser, B., & Weigl, A. (2015). Regression verification for programmable logic controller software. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9407, pp. 234–251). Springer Verlag. https://doi.org/10.1007/978-3-319-25423-4_15
Mendeley helps you to discover research relevant for your work.