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.
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2014 |
| Autor(en): | Thüm, Thomas ; Meinicke, Jens ; Benduhn, Fabian ; Hentschel, Martin ; Rhein, Alexander von ; Saake, Gunter |
| Art des Eintrags: | Bibliographie |
| Titel: | Potential Synergies of Theorem Proving and Model Checking for Software Product Lines |
| Sprache: | Englisch |
| Publikationsjahr: | September 2014 |
| Verlag: | ACM |
| Buchtitel: | Proceedings of the International Software Product Line Conference (SPLC) |
| Reihe: | SPLC |
| Kurzbeschreibung (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. |
| Freie Schlagworte: | Software product lines, theorem proving, model checking, design by contract, feature-based specification, family-based verification, variability encoding, feature-oriented contracts |
| ID-Nummer: | TUD-CS-2014-0930 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 31 Dez 2016 10:40 |
| Letzte Änderung: | 27 Jul 2021 16:02 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum