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

Revision: r1.1 - 07 Aug 2012 - 17:02 - WalterBinder
GPCE14 > P11Thum
Copyright © 1999-2020 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback