Advertisement

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)

Abstract

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.

Keywords

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

References

  1. 1.
    Apel, S., Batory, D.S., Kästner, C., Saake, G.: Springer. Feature-Oriented Software Product Lines (2013).  https://doi.org/10.1007/978-3-642-37521-7CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-22969-0_24CrossRefGoogle 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).  https://doi.org/10.1016/j.scico.2018.09.006CrossRefGoogle 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).  https://doi.org/10.1145/3336294.3336295
  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).  https://doi.org/10.1016/j.jlamp.2015.11.006MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    ter Beek, M.H., Mazzanti, F.: VMC: recent advances and challenges ahead. In: SPLC, pp. 70–77. ACM (2014).  https://doi.org/10.1145/2647908.2655969
  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).  https://doi.org/10.1007/978-3-642-32759-9_36CrossRefGoogle 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).  https://doi.org/10.1007/978-3-662-54494-5_23CrossRefGoogle 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).  https://doi.org/10.1016/j.scico.2015.06.005CrossRefGoogle 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).  https://doi.org/10.1109/TSE.2012.86CrossRefGoogle 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).  https://doi.org/10.1145/1806799.1806850
  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).  https://doi.org/10.1145/2499777.2499781
  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).  https://doi.org/10.1007/978-3-319-23404-5_18CrossRefGoogle Scholar
  14. 14.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE (1988).  https://doi.org/10.1109/LICS.1988.5119
  15. 15.
    Pohl, K., Böckle, G., van der Linden, F.: Software Product Line Engineering. Springer (2005).  https://doi.org/10.1007/3-540-28901-1CrossRefGoogle Scholar
  16. 16.
    Varshosaz, M., Beohar, H., Mousavi, M.: Basic behavioral models for software product lines: revisited. Sci. Comput. Program. 168, 171–185 (2018).  https://doi.org/10.1016/j.scico.2018.09.001CrossRefGoogle 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).  https://doi.org/10.1016/j.jlamp.2019.03.003MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

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

Personalised recommendations