KIT | KIT-Bibliothek | Impressum | Datenschutz

Verification of Software Product Lines with Delta-Oriented Slicing

Bruns, Daniel; Klebanov, Vladimir; Schaefer, Ina

Abstract:
Software product lines (SPL) are a well-known methodology to develop industry-size adaptable software systems. SPL are often used in domains where high-quality software is desirable, but the overwhelming product diversity remains a challenge for assuring correctness. We present our work in progress on reducing the deductive verification effort across different products of an SPL. On the specification side, our approach enriches the delta language for describing SPLs with formal product specifications. On the verification side, we combine program slicing and similarity-guided proof reuse to ease the verification process.


Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Proceedingsbeitrag
Jahr 2011
Sprache Englisch
Identifikator ISBN: 978-3-642-18069-9
ISSN: 0302-9743
KITopen ID: 1000024827
Erschienen in Formal Verification of Object-Oriented Software. International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010. Ed.: B. Beckert
Verlag Berlin, Springer
Seiten 61-75
Serie Lecture Notes in Computer Science ; 6528
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page