Feature interactions have been a major challenge of FOSD. Because of the crosscutting nature of features and the multiplicity of possible feature combinations, the detection of feature interactions is cumbersome. The idea of SpeK is to use formal specification to be able to reason automatically about which feature interactions are considered as flaws. We focus on product lines for which specifications are given for individual features, in contrast to scenarios, in which there is one specification for the entire product line.
SpeK brings support for composition of JML specifications to FeatureHouse. The combined code of every product can be checked against its combined specification, either by run-time assertion checking or by formal verification at compile-time.
We use the prover framework ESC/Java2 in combination with the prover Simplify to check if the combined code of a product complies with the output of SpeK.
The Java sources of the tool prototype SpeK are available.
In order to get started, download and unzip the distribution files.
The following example suggests that you place the FeatureHouse.jar in the base directory of the project you want to compose.
Open a terminal, cd to the directory and type:
SpeK is being developed at the University of Passau, Germany. For more information please contact the developers:
