WG211/M8Schaeffer
Software Product Lines
Ina Schaeffer
A software product line is a set of systems with well-defined commonalities and variabilities. Because of the huge number of possible configurations, it is crucial to guarantee critical system requirements. However, it is infeasible to formally verify each system in isolation. Instead, verification artifacts, i.e., properties and their proofs, should be reused in same way as other development artifacts.
In this talk, I present the concept of proof reuse for the efficient verification of software product lines. The presented approach is based on delta-modeling, a general technique to capture feature-based variability of software product lines. A set of systems is represented by a core system and a set of system deltas modifying the core to create other systems. The delta-modeling structure can be exploited to determine the reuse potential for proofs of system properties. This will be illustrated using the KeY verification system for Java.