TU Darmstadt / ULB / TUbiblio

Family-Based Deductive Verification of Software Product Lines

Thüm, Thomas and Schaefer, Ina and Apel, Sven and Hentschel, Martin (2012):
Family-Based Deductive Verification of Software Product Lines.
In: Proceedings of the 11th International Conference on Generative Programming and Component Engineering, ACM, Dresden, Germany, In: GPCE '12, ISBN 978-1-4503-1129-8,
[Conference or Workshop Item]

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

Item Type: Conference or Workshop Item
Erschienen: 2012
Creators: Thüm, Thomas and Schaefer, Ina and Apel, Sven and Hentschel, Martin
Title: Family-Based Deductive Verification of Software Product Lines
Language: German
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 %.

Title of Book: Proceedings of the 11th International Conference on Generative Programming and Component Engineering
Series Name: GPCE '12
Publisher: ACM
ISBN: 978-1-4503-1129-8
Uncontrolled Keywords: deductive verification, product-line analysis, program families, software product lines, theorem proving
Divisions: 20 Department of Computer Science > Software Engineering
20 Department of Computer Science
Event Location: Dresden, Germany
Date Deposited: 31 Dec 2016 10:40
Identification Number: TUD-CS-2012-0355
Export:

Optionen (nur für Redakteure)

View Item View Item