Regression verification for programmable logic controller software

Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, Alexander Weigl

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

23 Scopus citations

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.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages234-251
Number of pages18
DOIs
StatePublished - 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9407
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Automated production systems
  • Programmable logic controllers (PLC)
  • Regression verification
  • Symbolic model checking

Fingerprint

Dive into the research topics of 'Regression verification for programmable logic controller software'. Together they form a unique fingerprint.

Cite this