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