A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory Automation

Reviewed Paper In Proceedings

Author(s):Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Michael Kirsten, Franziska Wiebe, Bernhard Beckert, and Birgit Vogel‑Heuser
In:IEEE International Symposium on Assembly and Manufacturing (ISAM 2016)
Year:2016
Pages:19-25
DOI:10.1109/ISAM.2016.7750714

Abstract

Automated production systems (aPS) are complex systems with high reliability standards which can – besides through traditional testing – be ensured by verification using formal methods. In this paper we present a development process for aPS software supported by efficient formal techniques with easy-to-use specification formalisms to incease applicability in the aPS engineering domain. Our approach is tailored to the development of evolving aPS as existing behavior of earlier system revisions is reused as specification for the verification. The approach covers three verification phases: regression verification, verification of critical interlock invariants and delta specification and verification. The approach is designed to be comprehensible by aPS software engineers: Two practically applicable specification means are presented.
Formal methods have not yet been widely adapted in industrial aPS development since they lack (a) scalability, and (b) concise and comprehensible specification means. This paper shows concepts how to tackle both issues by referring to existing behavior during evolution verification to advance towards the goal of applicability in the aPS engineering domain.
A laboratory case study demonstrates the feasibility and performance of the approach and shows promising results.

BibTeX

@InProceedings{UlewiczUlbrichEtAl2016,
  author                = {Sebastian Ulewicz and Mattias Ulbrich and
                           Alexander Weigl and Michael Kirsten and Franziska Wiebe and
                           Bernhard Beckert and Birgit Vogel-Heuser},
  title                 = {A Verification-Supported Evolution Approach to Assist
                           Software Application Engineers in Industrial Factory Automation},
  booktitle             = {IEEE International Symposium on Assembly and
                           Manufacturing (ISAM 2016)},
  month                 = aug,
  year                  = {2016},
  abstract              = {Automated production systems (aPS) are complex systems
                           with high reliability standards which can -- besides through traditional
                           testing -- be ensured by verification using formal methods.
                           In this paper we present a development process for aPS software
                           supported by efficient formal techniques with easy-to-use specification
                           formalisms to incease applicability in the aPS engineering domain.
                           Our approach is tailored to the development of evolving aPS as existing
                           behavior of earlier system revisions is reused as specification for the
                           verification.
                           The approach covers three verification phases: regression verification,
                           verification of critical interlock invariants and delta specification
                           and verification.
                           The approach is designed to be comprehensible by aPS software engineers:
                           Two practically applicable specification means are presented.
                           \newline

                           Formal methods have not yet been widely adapted in industrial aPS
                           development since they lack (a) scalability, and (b) concise and
                           comprehensible specification means.
                           This paper shows concepts how to tackle both issues by referring to
                           existing behavior during evolution verification to advance towards the
                           goal of applicability in the aPS engineering domain.
                           \newline

                           A laboratory case study demonstrates the feasibility and performance of
                           the approach and shows promising results.},
  month                 = aug,
  year                  = {2016},
  pages                 = {19--25},
  date                  = {August 21-22},
  place                 = {Fort Worth, TX, USA},
  doi                   = {10.1109/ISAM.2016.7750714}
}