Paper Info
Title
Potential synergies of theorem proving and model checking for software product lines
Abstract
The verification of software product lines is an active research area. A challenge is to efficiently verify similar products without the need to generate and verify them individually. As solution, researchers suggest family-based verification approaches, which either transform compile-time into runtime variability or make verification tools variability-aware. Existing approaches either focus on theorem proving, model checking, or other verification techniques. For the first time, we combine theorem proving and model checking to evaluate their synergies for product-line verification. We provide tool support by connecting five existing tools, namely FeatureIDE and FeatureHouse for product-line development, as well as KeY, JPF, and OpenJML for verification of Java programs. In an experiment, we found the synergy of improved effectiveness and efficiency, especially for product lines with few defects. Further, we experienced that model checking and theorem proving are more efficient and effective if the product line contains more defects.
Year
DOI
Venue
2014
10.1145/2648511.2648530
SPLC
Keywords
Field
DocType
feature-oriented contracts,design,design by contract,software product lines,model checking,verification,family-based verification,languages,reusable software,theorem proving,feature-based specification,variability encoding
Functional verification,Model checking,Computer science,Design by contract,Automated theorem proving,Automated proof checking,Theoretical computer science,Runtime verification,High-level verification,Software verification
Conference
Citations 
PageRank 
References 
10
0.48
51
Authors
6
Name
Order
Citations
PageRank
Thomas Thüm1104847.15
Jens Meinicke231213.06
Fabian Benduhn32158.15
Martin Hentschel 00024100.48
Alexander von Rhein531611.35
Gunter Saake63255639.75