Counterexamples Guided Abstraction Refinement for Product-Line Behavioural Models
We recently designed abstraction techniques to address the state explosion problem well-known in model checking. We distinguish between three kinds of abstractions:
- feature abstraction abstracts variability information to make a given behaviour available to more products;
- state abstraction merges states, and consequently reduces the size of the state space;
- mixed abstraction combines the above two methods.
These advanced verification techniques have been implemented as new prototype variants of ProVeLines. We evaluated their benefits through experiments that tend to show substantial performance gains.
To install and use these new model checking algorithms, first download ProVeLines. Then, download this archive and extract its content into the src directory. Open configure.h and build.sh and do the following:
- To enable feature abstraction, enable the CEGARTRANS option and disable the CEGAR option in configure.h; then uncomment line 92 in build.sh.
- To enable state abstraction, enable the CEGAR option and disable the CEGARTRANS option in configure.h; then uncomment line 93 in build.sh.
- To enable mixed abstraction, enable both CEGARTRANS and CEGAR options in configure.h; then uncomment line 94 in build.sh.
Leave the other options of configure.h disabled. Then follows steps 5 to 7 of the installation guide. You’re done!
The evaluation results can be found here