Thüm, Thomas ; Schaefer, Ina ; Apel, Sven ; Hentschel, Martin (2012)
Family-Based Deductive Verification of Software Product Lines.
Dresden, Germany
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used off-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85 %.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2012 |
| Autor(en): | Thüm, Thomas ; Schaefer, Ina ; Apel, Sven ; Hentschel, Martin |
| Art des Eintrags: | Bibliographie |
| Titel: | Family-Based Deductive Verification of Software Product Lines |
| Sprache: | Deutsch |
| Publikationsjahr: | September 2012 |
| Verlag: | ACM |
| Buchtitel: | Proceedings of the 11th International Conference on Generative Programming and Component Engineering |
| Reihe: | GPCE '12 |
| Veranstaltungsort: | Dresden, Germany |
| Kurzbeschreibung (Abstract): | A software product line is a set of similar software products that share a common code base. While software product lines can be implemented efficiently using feature-oriented programming, verifying each product individually does not scale, especially if human effort is required (e.g., as in interactive theorem proving). We present a family-based approach of deductive verification to prove the correctness of a software product line efficiently. We illustrate and evaluate our approach for software product lines written in a feature-oriented dialect of Java and specified using the Java Modeling Language. We show that the theorem prover KeY can be used off-the-shelf for this task, without any modifications. Compared to the individual verification of each product, our approach reduces the verification time needed for our case study by more than 85 %. |
| Freie Schlagworte: | deductive verification, product-line analysis, program families, software product lines, theorem proving |
| ID-Nummer: | TUD-CS-2012-0355 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik > Software Engineering 20 Fachbereich Informatik |
| Hinterlegungsdatum: | 31 Dez 2016 10:40 |
| Letzte Änderung: | 16 Mai 2018 12:06 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum