A Verification-Supported Evolution Approach to Assist Software Application
Engineers in Industrial Factory Automation
Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Michael Kirsten,
Franziska Wiebe, Bernhard Beckert, and Birgit Vogel-Heuser
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.