The Elevator example originated from the work of Plath and Ryan [1], and was further processed by Classen et al. from the University of Namur[2], who provided a way to compose the features into a single FTS, and also made the number of floors a parameter, allowing the composition of different model sizes.
Classen et al's model and tools can be downloaded from the "Feature Transition Systems" webpage. For our experiments, we used the tools to create an Elevator consisting of 8 floors and all of the 9 features.
The Telephone example was also originated from the work of Plath and Ryan. The model can be downloaded from Ryan's homepage, look for "Code to support the paper" in "Feature Integration Using a Feature Construct". Or, directly download from: ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/00-scp-data.tar.gz
The code of the telephone is written in CMU SMV, and cannot be accepted by NuSMV. We manually converted the CMU SMV code into the NuSMV dialect. We thus do not guarantee compliance with the original semantics. We used Classen et al's composer to compose 7 features into a single FTS.
This example was inspired by an automotive feature requirements document. It was developed into an SMV model in the University of Waterloo, by David Dietrich, Pourya Shaker and Sandy Beidu. Note that nothing in this model can be attributed to the original document.
[1] M. Plath and M. D. Ryan. Feature Integration using a Feature Construct. Science of Computer Programming. 41(1), pp. 53-84.
[2] Classen, A.; Heymans, P.; Schobbens, P-Y. and Legay, A. Symbolic Model Checking of Software Product Lines. In 33rd International Conference on Software Engineering, ICSE 2011, May 21-28, 2011, pp. 321-330.