KIT | KIT-Bibliothek | Impressum | Datenschutz

Regression Verification for Programmable Logic Controller Software

Beckert, Bernhard ORCID iD icon; Ulbrich, Mattias ORCID iD icon; Vogel-Heuser, Birgit; Weigl, Alexander ORCID iD icon

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.


Volltext §
DOI: 10.5445/IR/1000047251
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 2015
Sprache Englisch
Identifikator ISSN: 2190-4782
urn:nbn:de:swb:90-472515
KITopen-ID: 1000047251
Verlag Karlsruher Institut für Technologie (KIT)
Umfang 16 S.
Serie Karlsruhe Reports in Informatics ; 2015,6
Projektinformation KASTEL_SKI (BMBF, 16KIS0843)
Schlagwörter regression verification, symbolic model checking, automated, production systems, programmable logic controllers (PLC)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page