Formal Verification of Evolutionary Changes

Book Chapter

Author(s):Bernhard Beckert, Jakob Mund, Mattias Ulbrich, and Alexander Weigl
In:Managed Software Evolution
Publisher:Springer
Year:2019
Pages:309-332
URL:https://doi.org/10.1007/978-3-030-13499-0_11
DOI:10.1007/978-3-030-13499-0_11

Abstract

In this chapter, we elaborate how formal verification techniques can be used to ensure safety properties of automated production systems during their evolution. First, we discuss the opportunities that formal methods offer, particularly when dealing with the evolution of automated production systems, but also which special needs this particular domain requires from the formal methods to be applied. We exemplarily present three approaches that successfully incorporate a formal verification technique for analysis, modelling, or reasoning into the system evolution process, namely, regression verification, generalised test tables, and model checking of holistic (multidomain) models.

BibTeX

@incollection{BeckertMUW19,
  author    = {Bernhard Beckert and
               Jakob Mund and
               Mattias Ulbrich and
               Alexander Weigl},
  editor    = {Ralf H. Reussner and
               Michael Goedicke and
               Wilhelm Hasselbring and
               Birgit Vogel{-}Heuser and
               Jan Keim and
               Lukas M{\"{a}}rtin},
  title     = {Formal Verification of Evolutionary Changes},
  booktitle = {Managed Software Evolution},
  pages     = {309--332},
  publisher = {Springer},
  year      = {2019},
  month     = jun,
  doi       = {10.1007/978-3-030-13499-0\_11}
}