Using SPLverifier Java Version (HowTo)

Version for the paper:
Strategies for Product-Line Verification: Case Studies and Experiments

This page describes the tool we used for the Java-based experiments in our paper "Strategies for Product-Line Verification: Case Studies and Experiments".
The files that are necessary for rereplication of our results are available as an archive below.

The archive contains the verified systems, the verification framework (as a JAR file), and the used model-checking tools JavaPathfinder (revision 635) and its extension jpf-bdd (revision 23). The framework that generates the products from a product line is not in the focus of this work, so include only the generated products in the archive. To verify the products, you only have to download the archive linked below (it includes all necessary tools).
The tool is designed to work in a GNU/Linux environment.

We compared the results of a sample-based verification strategy to the product- and family-based strategies. The archive contains information on the products of the sample sets.

Once you have extracted the archive, follow the below steps:

cd path-to-extracted-archive
java -jar ZipFileChecker.jar

This will create a new directory "results/" with the results of the verification runs.

Download

• Verification environment (includes the systems email, minepump and elevator and all necessary tools)
• Verification environment for AJStats (includes the system and all necessary tools)
• Verification environment for GPL (includes the system and all necessary tools)
• Benchmark files for GPL
• Verification environment for Zipme (includes the system and all necessary tools)


• Unprocessed features of all product lines (Java versions).


• Setup for experiments with deactivated specifications.