Regression verification for programmable logic controller software (bibtex)
by Beckert, Bernhard, Ulbrich, Mattias, Vogel-Heuser, Birgit and Weigl, Alexander
Abstract:
\textcopyright Springer International Publishing Switzerland 2015. 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.
Reference:
Regression verification for programmable logic controller software (Beckert, Bernhard, Ulbrich, Mattias, Vogel-Heuser, Birgit and Weigl, Alexander), Technical report 2015-06, Karlsruhe Institute of Technology, Department of Informatics, volume 9407, 2015.
Bibtex Entry:
@techreport{BeckertUlbrichVogelHeuser2015,
abstract = {{\textcopyright} Springer International Publishing Switzerland 2015. 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.},
author = {Beckert, Bernhard and Ulbrich, Mattias and Vogel-Heuser, Birgit and Weigl, Alexander},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
doi = {10.1007/978-3-319-25423-4_15},
institution = {Karlsruhe Institute of Technology, Department of Informatics},
isbn = {9783642209246},
issn = {16113349},
keywords = {Automated production systems,Programmable logic controllers (PLC),Regression verification,Symbolic model checking,improve-aps,improve-aps_pw},
mendeley-tags = {improve-aps,improve-aps_pw},
number = {2015-06},
pages = {234--251},
title = {{Regression verification for programmable logic controller software}},
volume = {9407},
year = {2015}
}
Powered by bibtexbrowser