This page describes the tool we used for the C-based experiments in our paper "Strategies for Product-Line Verification: Case Studies and Experiments".
The files that are necessary for replication of our results are available as an archive below.
The archive contains the verified systems (already pre-processed by CIL) and some configuration files for CPAchecker (the model-checking tool we used in the experiments for C). The framework that generates the products from a product line is not in the focus of this work, so we include only the generated products in the archive. To verify the products, you have to download CPAchecker from here. We used the SVN revision 5540 of the branch "explicit" for our experiments.
We compared the results of different sample-based verification strategies to the product- and family-based strategies. The sample-based strategies are: single-wise, pair-wise and triple-wise. The archive contains information on the products contained in the sample sets.
Once you have extracted the archive and CPAchecker is downloaded and working, follow the these steps:
Replace the string "PATH-TO-THIS-DIRECTORY" in the two XML-files with the path to the extracted archive (the path where the XML files are).
Then start the verification with the CPAchecker benchmark script:
cd CPAcheckerDIR
python ./scripts/benchmark.py path-to-extracted-archive/productBased.xml
python ./scripts/benchmark.py path-to-extracted-archive/familyBased.xml
In Section 3 of the paper, we measure the similarity degree of the sample systems based on executed instructions. For these experiments, we used the same sample systems, with deactivated specifications. Because the specifications are not active the systems are always "SAFE" and the complete state space has to be explored. The systems for these experiments are available below. To log the number of executed CFA edges you have to replace two classes in CPAchecker with the ones given below.