Vortragende(r): Dr. Ina Schaefer
(Chalmers University, Gothenburg, Sweden)
Achtung! Kolloquium ausser der Reihe!
Das Kolloquium beginnt bereits um 16 Uhr c.t. !
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 our work on 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.