SPLverifier: Model Checking of Software Product Lines

Overview





Uni Logo

Software Product Line Group

Software Systems Lab

Using SPLverifier (HowTo)

Version for the paper:
Detection of Feature Interactions using Feature-Aware Verification
International Conference on Automated Software Engineering (ASE)
November 2011 (to appear)

The tool chain was developed and tested on Ubuntu Linux 10.4 and requires the following packages to be installed:

python build-essential python java sun-java6-jdk python-pip cbmc

After that, additional python packages need to be installed:

pip install colorama
pip install fabric

Then download and unpack SPLverifier in a directory of your choice and cd to that directory.

You can verify the email system by issuing the following command:

fab check_emailsystem

This command performs the checks on the email system using the CBMC model checker. Without arguments check_emailsystem checks all generated variants and the variability encoded product line using one specification at a time.

To check only the variability encoded product line run:

fab check_emailsystem:variants=0,ve=1

To check all variants but not the variability encoded product line run:

fab check_emailsystem:variants=1,ve=0

The commands above use scenarios, in which bugs are present. To use the safe scenarios append scenarios=safe to the commands above, e.g. to check the safe scenarios using variability encoding run:

fab check_emailsystem:variants=0,ve=1,scenarios=safe

Download