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. In the first phase of the IMPROVE project, we have investigated the foundations of regression verification, developed the basic methods, and shown their applicability to realistic examples and case studies. In the second phase of the 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 the first phase of IMPROVE, we investigated regression verification for imperative programs in general and for object-oriented programs in particular. In the second 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 sys-tems (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.

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 Karlsruhe Institute of Technology (KIT) and the Technische Universität München (TUM).

Persons

Related Publications

Höhere Softwarequalität in Automatisierungsanwendungen (Link)
B. Vogel-Heuser and S. Cha, In: Embedded Software Engineering (Vogel Communications Group),  Feb. 2020.

Applicability of Generalized Test Tables: A Case Study Using the Manufacturing System Demonstrator xPPU
S. Cha, A. Weigl, M. Ulbrich, B. Beckert and B. Vogel-Heuser, In: Automatisierungstechnik (at), Oct. 2018.

Generalised Test Tables – a Practical Specification Language for Reactive Systems
B. Beckert, S. Cha, M. Ulbrich, B. Vogel-Heuser and A. Weigl, In: 13th International Conference on integrated (iFM 2017), Springer, Sep. 2017.

A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory Automation
S. Ulewicz, M. Ulbrich, A. Weigl, M. Kirsten, F. Fassl, B. Beckert, B. Vogel-Heuser, In: IEEE International Symposium on Assembly and Manufacturing (ISAM), Fort Worth, USA, 2016.

Regression Verification for Programmable Logic Controller Software
B. Beckert, M. Ulbrich, B. Vogel-Heuser, A. Weigl
In: The 17th International Conference on Formal Engineering Methods (ICFEM 2015)

Proving Equivalence between Control Software Variants for Programmable Logic Controllers
S. Ulewicz, B. Vogel-Heuser, M. Ulbrich, A. Weigl, B. Beckert
In: 20th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2015)

Selected challenges of software evolution for automated production systems
B. Vogel-Heuser, S. Feldmann, J. Folmer, M. Kowal, I. Schaefer, J. Ladiges, A. Fay, C. Haubeck, W. Lamersdorf, S. Lity, T. Kehrer, M. Tichy, S. Getir, M. Ulbrich, V. Klebanov, B. Beckert
In: 13th International Conference on Industrial Informatics (INDIN 2015)