Journal
ACM SIGPLAN NOTICES
Volume 48, Issue 3, Pages 11-20Publisher
ASSOC COMPUTING MACHINERY
DOI: 10.1145/2480361.2371404
Keywords
Reliability; Verification; Product-line analysis; software product lines; program families; deductive verification; theorem proving
Categories
Funding
- German Research Foundation [DFG - SCHA 1635/2-1, DFG - AP 206/2, AP 206/4, LE 912/13]
- European Union [EU - FP7-231620 HATS]
Ask authors/readers for more resources
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 %.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available