Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints

  • Maurice H. ter BeekEmail author
  • Ferruccio Damiani
  • Stefania Gnesi
  • Franco Mazzanti
  • Luca Paolini
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11918)


Modal transition systems (MTSs) and featured transition systems (FTSs) are widely recognised as fundamental behavioural models for software product lines. This short paper summarises the contributions published in [3]: MTSs with variability constraints (MTS\(\upsilon \)s) are equally expressive as FTSs. This is proved by giving sound and complete transformations of the latter into the former, and of the former into the latter. The benefits of this result are twofold. First, it contributes to the expressiveness hierarchy of such basic models studied in the literature. Second, it provides an automatic algorithm from FTSs to MTS\(\upsilon \)s that preserves the original (compact) branching structure, thus paving the way for model checking FTSs with the variability model checker VMC.


SPL Variability Behavioural model Formal specification Featured transition system Modal transition system 


  1. 1.
    Apel, S., Batory, D.S., Kästner, C., Saake, G.: Springer. Feature-Oriented Software Product Lines (2013). Scholar
  2. 2.
    ter Beek, M.H., Damiani, F., Gnesi, S., Mazzanti, F., Paolini, L.: From featured transition systems to modal transition systems with variability constraints. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 344–359. Springer, Cham (2015). Scholar
  3. 3.
    ter Beek, M.H., Damiani, F., Gnesi, S., Mazzanti, F., Paolini, L.: On the expressiveness of modal transition systems with variability constraints. Sci. Comput. Program. 169, 1–17 (2019). Scholar
  4. 4.
    ter Beek, M.H., Damiani, F., Lienhardt, M., Mazzanti, F., Paolini, L.: Static analysis of featured transition systems. In: SPLC, pp. 39–51. ACM (2019).
  5. 5.
    ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebr. Meth. Program. 85(2), 287–315 (2016). Scholar
  6. 6.
    ter Beek, M.H., Mazzanti, F.: VMC: recent advances and challenges ahead. In: SPLC, pp. 70–77. ACM (2014).
  7. 7.
    ter Beek, M.H., Mazzanti, F., Sulova, A.: VMC: a tool for product variability analysis. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 450–454. Springer, Heidelberg (2012). Scholar
  8. 8.
    ter Beek, M.H., de Vink, E.P., Willemse, T.A.C.: Family-based model checking with mCRL2. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 387–405. Springer, Heidelberg (2017). Scholar
  9. 9.
    Beohar, H., Varshosaz, M., Mousavi, M.: Basic behavioral models for software product lines: expressiveness and testing pre-orders. Sci. Comput. Program. 123, 42–60 (2016). Scholar
  10. 10.
    Classen, A., Cordy, M., Schobbens, P.-Y., Heymans, P., Legay, A., Raskin, J.F.: Featured transition systems: foundations for verifying variability-intensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069–1089 (2013). Scholar
  11. 11.
    Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A., Raskin, J.-F.: Model checking \( {\text{lots}}\) of systems: efficient verification of temporal properties in software product lines. In: ICSE, pp. 335–344. ACM (2010).
  12. 12.
    Cordy, M., Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: ProVeLines: a product line of verifiers for software product lines. In: SPLC, pp. 141–146. ACM (2013).
  13. 13.
    Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wąsowski, A.: Family-based model checking without a family-based model checker. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 282–299. Springer, Cham (2015). Scholar
  14. 14.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE (1988).
  15. 15.
    Pohl, K., Böckle, G., van der Linden, F.: Software Product Line Engineering. Springer (2005). Scholar
  16. 16.
    Varshosaz, M., Beohar, H., Mousavi, M.: Basic behavioral models for software product lines: revisited. Sci. Comput. Program. 168, 171–185 (2018). Scholar
  17. 17.
    Varshosaz, M., Luthmann, L., Mohr, P., Lochau, M., Mousavi, M.: Modal transition system encoding of featured transition systems. J. Log. Algebr. Meth. Program. 106, 1–28 (2019). Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.ISTI–CNRPisaItaly
  2. 2.University of TurinTurinItaly

Personalised recommendations