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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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-7
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_24
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.006
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
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.006
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
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_36
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_23
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.005
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.86
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
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
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_18
Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE (1988). https://doi.org/10.1109/LICS.1988.5119
Pohl, K., Böckle, G., van der Linden, F.: Software Product Line Engineering. Springer (2005). https://doi.org/10.1007/3-540-28901-1
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.001
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.003
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
ter Beek, M.H., Damiani, F., Gnesi, S., Mazzanti, F., Paolini, L. (2019). Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints. In: Ahrendt, W., Tapia Tarifa, S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science(), vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_34
Download citation
DOI: https://doi.org/10.1007/978-3-030-34968-4_34
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-34967-7
Online ISBN: 978-3-030-34968-4
eBook Packages: Computer ScienceComputer Science (R0)