Thüm, Thomas ; Meinicke, Jens ; Benduhn, Fabian ; Hentschel, Martin ; Rhein, Alexander von ; Saake, Gunter (2014)
Potential Synergies of Theorem Proving and Model Checking for Software Product Lines.
Conference or Workshop Item, Bibliographie
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 ; Meinicke, Jens ; Benduhn, Fabian ; Hentschel, Martin ; Rhein, Alexander von ; Saake, Gunter |
| Type of entry: | Bibliographie |
| Title: | Potential Synergies of Theorem Proving and Model Checking for Software Product Lines |
| Language: | English |
| Date: | September 2014 |
| Publisher: | ACM |
| Book Title: | Proceedings of the International Software Product Line Conference (SPLC) |
| Series: | SPLC |
| 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. |
| Uncontrolled Keywords: | Software product lines, theorem proving, model checking, design by contract, feature-based specification, family-based verification, variability encoding, feature-oriented contracts |
| Identification Number: | TUD-CS-2014-0930 |
| Divisions: | 20 Department of Computer Science 20 Department of Computer Science > Software Engineering |
| Date Deposited: | 31 Dec 2016 10:40 |
| Last Modified: | 27 Jul 2021 16:02 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Send an inquiry |
Options (only for editors)
 |
Show editorial Details |
Drucken
Impressum