Comparative Expressiveness of Product Line Calculus of Communicating Systems and 1-Selecting Modal Transition Systems

  • Mahsa VarshosazEmail author
  • Mohammad Reza Mousavi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11376)


Product line calculus of communicating systems (PL-CCSs) is a process calculus proposed to model the behavior of software product lines. Modal transition systems (MTSs) are also used to model variability in behavioral models. MTSs are known to be strictly less expressive than PL-CCS. In this paper, we show that the extension of MTSs with hyper transitions by Fecher and Schmidt, called 1-selecting modal transition systems (1MTSs), closes this expressiveness gap. To this end, we propose a novel notion of refinement for 1MTSs that makes them more suitable for specifying variability for software product lines and prove its various essential properties.


Product line calculus of communicating systems (PL-CCS) Modal transition system (MTSs) 1-selecting modal transition system (1MTS) Comparative expressiveness 


  1. 1.
    Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A model-checking tool for families of services. In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE -2011. LNCS, vol. 6722, pp. 44–58. Springer, Heidelberg (2011). Scholar
  2. 2.
    Asirelli, P., ter Beek, M.H., Gnesi, S., Fantechi, A.: Formal description of variability in product families. In: Proceedings of the 15th International Software Product Line Conference, SPLC 2011, pp. 130–139. IEEE (2011)Google Scholar
  3. 3.
    Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A compositional framework to derive product line behavioural descriptions. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 146–161. Springer, Heidelberg (2012). Scholar
  4. 4.
    Basile, D., ter Beek, M.H., Di Giandomenico, F., Gnesi, S.: Orchestration of dynamic service product lines with featured modal contract automata. In: Proceedings of the 21st International Systems and Software Product Line Conference, SPLC 2017, vol. B, pp. 117–122. ACM, New York (2017).
  5. 5.
    Basile, D., Di Giandomenico, F., Gnesi, S., Degano, P., Ferrari, G.L.: Specifying variability in service contracts. In: Proceedings of the Eleventh International Workshop on Variability Modelling of Software-Intensive Systems, VAMOS 2017, pp. 20–27. ACM, New York (2017).
  6. 6.
    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. Logic. Algebraic Methods Program. 85(2), 287–315 (2016)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Benduhn, F., Thüm, T., Lochau, M., Leich, T., Saake, G.: A survey on modeling techniques for formal behavioral verification of software product lines. In: Proceedings of the Ninth International Workshop on Variability Modelling of Software-Intensive Systems, VaMoS 2015, New York, NY, USA, pp. 80:80–80:87 (2015)Google Scholar
  8. 8.
    Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Parametric modal transition systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 275–289. Springer, Heidelberg (2011). Scholar
  9. 9.
    Beohar, H., Varshosaz, M., Mousavi, M.R.: Basic behavioral models for software product lines: expressiveness and testing pre-orders. Sci. Comput. Program. (2015, in press)Google 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)CrossRefGoogle Scholar
  11. 11.
    Classen, A., Heymans, P., Schobbens, P.Y., Legay, A., Raskin, J.F.: Model checking lots of systems: efficient verification of temporal properties in software product lines. In: Proceedings of the 32nd International Conference on Software Engineering, ICSE 2010, vol. 1, pp. 335–344. ACM (2010)Google Scholar
  12. 12.
    Fecher, H., Schmidt, H.: Comparing disjunctive modal transition systems with an one-selecting variant. J. Logic Algebraic Program. 77(1–2), 20–39 (2008)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Fischbein, D., Uchitel, S., Braberman, V.: A foundation for behavioural conformance in software product line architectures. In: Proceedings of the ISSTA Workshop on Role of Software Architecture for Testing and Analysis, pp. 39–48. ACM (2006)Google Scholar
  14. 14.
    Gruler, A., Leucker, M., Scheidemann, K.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 113–131. Springer, Heidelberg (2008). Scholar
  15. 15.
    Kang, K., Cohen, S., Hess, J., Novak, W., Peterson, S.: Feature-oriented domain analysis (FODA) feasibility study. Technical report CMU/SEI-90-TR-21. Software Engineering Institute, Carnegie Mellon University (1990)Google Scholar
  16. 16.
    Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007). Scholar
  17. 17.
    Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science, LICS 1990, pp. 108–117. IEEE Computer Society (1990).
  18. 18.
    Larsen, K., Thomsen, B.: A modal process logic. In: Proceedings of the 3rd Annual Symposium on Logic in Computer Science, LICS 1988, pp. 203–210. IEEE (1988)Google Scholar
  19. 19.
    Lochau, M., Kamischke, J.: Parameterized preorder relations for model-based testing of software product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 223–237. Springer, Heidelberg (2012). Scholar
  20. 20.
    Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). Scholar
  21. 21.
    Shoham, S., Grumberg, O.: Multi-valued model checking games. J. Comput. Syst. Sci. 78(2), 414–429 (2012)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Centre for Research on Embedded SystemsHalmstad UniversityHalmstadSweden
  2. 2.Department of InformaticsUniversity of LeicesterLeicesterUK

Personalised recommendations