TU Darmstadt / ULB / TUbiblio

Potential Synergies of Theorem Proving and Model Checking for Software Product Lines

Thüm, Thomas and Meinicke, Jens and Benduhn, Fabian and Hentschel, Martin and von Rhein, Alexander and Saake, Gunter (2014):
Potential Synergies of Theorem Proving and Model Checking for Software Product Lines.
In: Proceedings of the International Software Product Line Conference (SPLC), ACM, In: SPLC, [Conference or Workshop Item]

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 variabilityaware. 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.

Item Type: Conference or Workshop Item
Erschienen: 2014
Creators: Thüm, Thomas and Meinicke, Jens and Benduhn, Fabian and Hentschel, Martin and von Rhein, Alexander and Saake, Gunter
Title: Potential Synergies of Theorem Proving and Model Checking for Software Product Lines
Language: German
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 variabilityaware. 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.

Title of Book: Proceedings of the International Software Product Line Conference (SPLC)
Series Name: SPLC
Publisher: ACM
Uncontrolled Keywords: Software product lines, theorem proving, model checking, design by contract, feature-based specification, family-based verification, variability encoding, feature-oriented contracts
Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Date Deposited: 31 Dec 2016 10:40
Identification Number: TUD-CS-2014-0930
Export:

Optionen (nur für Redakteure)

View Item View Item