Ismayle S. Santos, Lincoln S. Rocha, Pedro A. Santos Neto, and Rossana M. C. Andrade. 2016. Model Verification of Dynamic Software Product Lines. In Proceedings of the 30th Brazilian Symposium on Software Engineering (SBES '16), ACM, New York, NY, USA, 113-122. DOI: http://dx.doi.org/10.1145/2973839.2973852

URL: http://dl.acm.org/citation.cfm?id=2973852

The DSPL model checking approach involves the following steps:

• STEP 01: Provide the DSPL Feature Model. In this case, the eCFM model specified in the eCFM tool
• STEP 02: Provide the context evolution model (Context Kripke Structure). This model is specified as a sequence of context states [1].
• STEP 03: Generate the promela file by using the eCFM Tool. This file will contain the Dynamic Feature Transition System (DFTS) in the promela language.
• STEP 04: Specify the proprieties to be verified in Linear Temporal Logic. The generated file already contains 5 generic proprieties, but the user can define other ones.
• STEP 05: Run the verification with the SPIN Model Checker tool. Spin tool available at http://spinroot.com/

An example of the promela file generated by the eCFM tool is available here. Bellow there is one screenshot during the model checking of property pro21.

References

[1] L. S. Rocha and R. M. C. Andrade. Towards a formal model to reason about context-aware exception handling. In Proceedings of the 5th International Workshop on Exception Handling, WEH ’12.