Modular Regression Verification for Reactive Systems

摘要

Reactive software is often deployed in long-running systems with high dependability requirements. Despite their safety- and mission-critical use, their functionalities must occasionally be adapted, for example to support new features or regulations. But software evolution bears the risk of introducing new malfunctions. Regression verification helps preventing the introduction of unintended, faulty behaviour. In this paper we present a novel approach for modular regression verification proofs for reactive systems based on the idea of relational regression verification contracts. The approach allows the decomposition of a larger regression verification proof into smaller proofs on its subcomponents. We embedded the decomposition rule in a new algorithm for regression verification, which orchestrates several light- and heavyweight techniques. We implemented our approach for software used by Programmable Logic Controllers (PLC) written in Structured Text (IEC611131-3) and show the potential of the approach with selected scenarios of a Pick-and-Place-Unit case study.