IMPROVE APS

Regression Verification in a User-Centered Software Development Process for Evolving Automated Production Systems

Project Description

The vision for this project is to advance technology such that regression verification methods are available that will be routinely used for ensuring correctness in the evolution processes for long-living reliable systems requiring frequent re-validation. The goal of regression verification is to formally prove that software remains correct through its evolution, changes have the desired effect, and no new bugs are introduced.
Regression verification avoids the main bottleneck for the routine practical use of formal verification, namely the need to write full functional specifications (which is a huge effort). Also, given two program versions or variants that are both complex but similar to each other, the effort for verifying the relation between them mainly depends on the difference between the programs and not on their overall size and complexity.

As a follow-up to the IMPROVE project, we plan to overcome the two remaining obstacles on the path to reaching the above vision of routine use:

• Reach and power: The reach and power of regression verification needs to be extended to cover real-world systems and change scenarios.
• User in the loop: Regression verification needs to be integrated into the software development and evolution process, and useful feedback needs to be given to the user in case a verification attempt is not immediately successful.

In this phase, we will target a particular application domain. This provides the third main motif for our project in Phase 2 – now called IMPROVE APS:

Automated production systems in the pharmaceutical and the food-manufacturing industry: The control software and discrete processes of automated production systems (aPS) are a very promising application area for regression verification. These systems are long-living and have to fulfill dependability and reliability criteria to avoid machine hazards or accidents involving operator or maintenance personnel. Applicability in realistic industrial situations is within reach as we focus on evolution with limited changes (e.g., bug fixes) and small variations in the software. As case studies, we use manufacturing systems in the pharmaceutical and the food industry, where aPS must be validated following regulations to ensure no harm is inflicted on consumers of the products.

The envisaged solutions of IMPROVE APS follow the goal of a comprehensive elaboration of approaches to manage software evolution with additional constraints from application taken into account.

This project is part of the DFG SPP1593 "Design for Future"

History

This project is the successor of the IMPROVE project, which focused on regression verification of imperative and object-oriented programs.
We have investigated the foundations of regression verification, developed the basic methods, and shown their applicability to realistic examples and case studies.

People

In line with the new focus on integration into the software development process and the application domain of automated production systems, IMPROVE APS has a new set of principal investigators and is now a collaboration of the Institute of Automation and Information Systems (led by Birgit Vogel-Heuser) at Technische Universität München (TUM) and the Application-oriented Formal Verification group (led by Bernhard Beckert) at Karlsruhe Institute of Technology (KIT).

Name	Role	Institution
Bernhard Beckert	Project Investigator	KIT
Birgit Vogel-Heuser	Project Investigator	TUM
Mattias Ulbrich	Project Investigator	KIT
Suhyun Cha	Funded Member	TUM
Alexander Weigl	Funded Member	KIT
Sebastian Ulewicz	Former Member	TUM
Michael Kirsten	Former Member	KIT
Franziska Wiebe	Former Member	TUM

Publications

2018

Title	Author(s)	Source
Applicability of Generalized Test Tables: A Case Study Using the Manufacturing System Demonstrator xPPU	Suhyun Cha, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert, and Birgit Vogel‑Heuser	Automatisierungstechnik Special Issue
Achieving delta description for the system software of an automated production evolution based on partially inferenced model	Suhyun Cha, Alexander Weigl, Mattias Ulbrich, Bernhard Beckert, and Birgit Vogel‑Heuser	14th IEEE International Conference on Automation Science and Engineering (CASE 2018)

2017

Title	Author(s)	Source
Generalised Test Tables: A Practical Specification Language for Reactive Systems	Bernhard Beckert, Suhyun Cha, Mattias Ulbrich, Birgit Vogel‑Heuser, and Alexander Weigl	13th International Conference on integrated Formal Methods (iFM 2017)
Generation of Monitoring Functions in Production Automation Using Test Specifications	Suhyun Cha, Sebastian Ulewicz, Birgit Vogel‑Heuser, Alexander Weigl, Mattias Ulbrich, and Bernhard Beckert	15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive Systems	Alexander Weigl, Franziska Wiebe, Mattias Ulbrich, Sebastian Ulewicz, Suhyun Cha, Michael Kirsten, Bernhard Beckert, and Birgit Vogel‑Heuser	15th IEEE International Conference on Industrial Informatics (INDIN 2017)

2016

Title	Author(s)	Source
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	IEEE International Symposium on Assembly and Manufacturing (ISAM 2016)

2017

Title	Author(s)	Source
Relational Program Reasoning Using Compiler IR – Combining Static Verification and Dynamic Analysis	Moritz Kiefer, Vladimir Klebanov, and Mattias Ulbrich	Journal of Automated Reasoning 60(3)

2015

Title	Author(s)	Source
Proving Equivalence between Control Software Variants for Programmable Logic Controllers - Using Regression Verification to Reduce Unneeded Variant Diversity	Sebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Bernhard Beckert, and Birgit Vogel‑Heuser	20th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2015)
Selected Challenges of Software Evolution for Automated Production Systems	Birgit Vogel‑Heuser, Stefan Feldmann, Jens Folmer, Matthias Kowal, Ina Schaefer, Jan Ladiges, Alexander Fay, Christopher Haubeck, Winfried Lamersdorf, Sascha Lity, Timo Kehrer, Matthias Tichy, Sinem Getir, Mattias Ulbrich, Vladimir Klebanov, and Bernhard Beckert	13th IEEE International Conference on Industrial Informatics (INDIN 2015)
Regression Verification for Java Using a Secure Information Flow Calculus	Bernhard Beckert, Vladimir Klebanov, and Mattias Ulbrich	17th Workshop on Formal Techniques for Java-like Programs (FTfJP 2015)
Regression Verification for Programmable Logic Controller Software	Bernhard Beckert, Mattias Ulbrich, Birgit Vogel‑Heuser, and Alexander Weigl	Karlsruhe Institute of Technology, Department of Informatics 2015-06
Automating Regression Verification	Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich	Multikonferenz Software Engineering und Management 2015: Fachtagung Software Engineering (SE 2015)
Regression Verification for Programmable Logic Controller Software	Alexander Sebastian Weigl	Karlsruhe Institute of Technology (January 2015)

2014

Title	Author(s)	Source
Automating Regression Verification	Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich	29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014)

Software

On request, we provide the toolchain presented at ICFEM '15. Feel free to contact Mattias Ulbrich for requests. For more information, please have a look at ReVe for PLC. Additionally, most software parts associated to our publications are open source; see VerifAPS or the github page.