TY - CHAP
T1 - Regression verification for programmable logic controller software
AU - Beckert, Bernhard
AU - Ulbrich, Mattias
AU - Vogel-Heuser, Birgit
AU - Weigl, Alexander
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
KW - Automated production systems
KW - Programmable logic controllers (PLC)
KW - Regression verification
KW - Symbolic model checking
UR - http://www.scopus.com/inward/record.url?scp=84949239519&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-25423-4_15
DO - 10.1007/978-3-319-25423-4_15
M3 - Chapter
AN - SCOPUS:84949239519
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 234
EP - 251
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PB - Springer Verlag
ER -