Skip to main content
SpringerLink
Log in

Model Checking Value-Passing Modal Specifications

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8974))

Abstract

Formal modelling and verification of variability concepts in product families has been the subject of extensive study in the literature on Software Product Lines. In recent years, we have laid the basis for the use of modal specifications and branching-time temporal logics for the specification and analysis of behavioural variability in product family definitions. A critical point in this formalization is the lack of a possibility to model an adequate representation of the data that may need to be described when considering real systems. To this aim, we now extend the modelling and verification environment that we have developed for specifications interpreted over Modal Transition Systems, by adding the possibility to include data in the specifications. In concert with this, we also extend the variability-specific modal logic and the associated special-purpose model checker VMC. As a result, it offers the possibility to efficiently verify formulas over possibly infinite-state systems by using the on-the-fly bounded model-checking algorithms implemented in the model checker. We illustrate our approach by means of a simple yet intuitive example: a bike-sharing system.

Research partly supported by the EU FP7-ICT FET-Proactive project QUANTICOL (600708) and by the Italian MIUR project CINA (PRIN 2010LHT4KM).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Actually, each product moreover needs to satisfy assumptions of coherence and consistency and variability constraints of the form alternative, excludes, and requires [9].

  2. 2.

    In VMC, \(\lnot \), \(\vee \), \(\wedge \), \([\,]^{\Box }\), \(\mu \), \(\nu \), and \(F^{\Box }\) are written as not, or, and, []#, min, max, and F#, respectively, whereas ‘* ’ can be used as ‘don’t care’ symbol for parameter values.

  3. 3.

    In VMC, text or code can be commented out by prefixing it with --.

References

  1. Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wąsowski, A.: 20 Years of modal and mixed specifications. Bull. EATCS 95, 94–129 (2008)

    MATH  Google Scholar 

  2. Åqvist, L.: Deontic logic. Handbook of Philosophical Logic, 2nd edn, pp. 147–264. Kluwer, Dordrecht (2002)

    Chapter  Google Scholar 

  3. Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A logical framework to deal with variability. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 43–58. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  4. Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: Formal description of variability in product families. In: SPLC 2011, pp. 130–139. IEEE (2011)

    Google Scholar 

  5. ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011)

    Article  MATH  Google Scholar 

  6. ter Beek, M.H., Gnesi, S., Mazzanti, F.: Demonstration of a model checker for the analysis of product variability. In: SPLC 2012, pp. 242–245. ACM (2012)

    Google Scholar 

  7. ter Beek, M.H., Lluch Lafuente, A., Petrocchi, M.: Combining declarative and procedural views in the specification and analysis of product families. In: SPLC 2013, Vol. 2, pp. 10–17. ACM (2013)

    Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. ter Beek, M.H., Mazzanti, F.: VMC: recent advances and challenges ahead. In: SPLC 2014, Vol. 2, pp. 70–77. ACM (2014)

    Google Scholar 

  10. ter Beek, M.H., de Vink. E.P.: Using mCRL2 for the analysis of software product lines. In: FormaliSE 2014, IEEE (2014)

    Google Scholar 

  11. ter Beek, M.H., de Vink, E.P.: Software product line analysis with mCRL2. In: SPLC 2014, vol. 2, pp. 78–85. ACM (2014)

    Google Scholar 

  12. ter Beek, M.H., de Vink, E.P.: Towards modular verification of software product lines with mCRL2. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 368–385. Springer, Heidelberg (2014)

    Google Scholar 

  13. Beneš, N., Černá, I., Křetínský, J.: Modal transition systems: composition and LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 228–242. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications. ACM TOPLAS 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  16. 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 TSE 39(8), 1069–1089 (2013)

    Google Scholar 

  17. DeMaio, P.: Bike-sharing: history, impacts, models of provision, and future. J. Public Transp. 12(4), 41–56 (2009)

    Article  MathSciNet  Google Scholar 

  18. De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  19. De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995)

    Article  MATH  Google Scholar 

  20. D’Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: the modal transition system analyser. In: ASE 2008, pp. 475–476. IEEE (2008)

    Google Scholar 

  21. Fantechi, A., Lapadula, A., Pugliese, R., Tiezzi, F., Gnesi, S., Mazzanti, F.: A logical verification methodology for service-oriented computing. ACM TOSEM 21(3), 1–46 (2012). Article 16

    Article  Google Scholar 

  22. Fischbein, D., Uchitel, S., Braberman, V.A.: A foundation for behavioural conformance in software product line architectures. In: ROSATEA 2006, pp. 39–48. ACM (2006)

    Google Scholar 

  23. Fricker, C., Gast, N.: Incentives and redistribution in homogeneous bike-sharing systems with stations of finite capacity. EURO J. Transp. Logistics, 1–31 (2014)

    Google Scholar 

  24. Gnesi, S., Petrocchi, M.: Towards an executable algebra for product lines. In: SPLC 2012, Vol. 2, pp. 66–73. ACM (2012)

    Google Scholar 

  25. Groote, J.F., Mateescu, R.: Verification of temporal properties of processes in a setting with data. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 74–90. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  26. Krka, I., Edwards, G., Brun, Y., Medvidovic, N.: From system specifications to component behavioral models. In: ICSE 2009, pp. 315–318. IEEE (2009)

    Google Scholar 

  27. Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoret. Comput. Sci. 72(2–3), 265–288 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  28. 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)

    Chapter  Google Scholar 

  29. Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS 1988, pp. 203–210. IEEE (1988)

    Google Scholar 

  30. Lauenroth, K., Pohl, K., Töhning, S.: Model checking of domain artifacts in product line engineering. In: ASE 2009, pp. 269–280. IEEE (2009)

    Google Scholar 

  31. Leucker, M., Thoma, D.: A formal approach to software product families. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 131–145. Springer, Heidelberg (2012)

    Google Scholar 

  32. Meolic, R., Kapus, T., Brezocnik, Z.: ACTLW: an action-based computation tree logic with unless operator. Inf. Sci. 178(6), 1542–1557 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  33. Milner, R.: Communication and Concurrency. Prentice Hall (1989)

    Google Scholar 

  34. Pohl, K., Böckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer, Heidelberg (2005)

    Book  Google Scholar 

  35. Sibay, G.E., Uchitel, S., Braberman, V., Kramer, J.: Distribution of modal transition systems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 403–417. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

Download references

Acknowledgments

We thank Marco Bertini from PisaMo S.p.A. for generously sharing with us his knowledge on bike-sharing systems in general and CicloPi in particular.

Author information

Authors and Affiliations

  1. ISTI–CNR, Via G. Moruzzi 1, Pisa, Italy

    Maurice H. ter Beek, Stefania Gnesi & Franco Mazzanti

Authors
  1. Maurice H. ter Beek
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefania Gnesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Franco Mazzanti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maurice H. ter Beek .

Editor information

Editors and Affiliations

  1. School of Computer Science, University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

  2. A.P. Ershov Institute of Informatics Systems, Novosibirsk, Russia

    Irina Virbitskaite

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

ter Beek, M.H., Gnesi, S., Mazzanti, F. (2015). Model Checking Value-Passing Modal Specifications. In: Voronkov, A., Virbitskaite, I. (eds) Perspectives of System Informatics. PSI 2014. Lecture Notes in Computer Science(), vol 8974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46823-4_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-46823-4_25

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-46822-7

  • Online ISBN: 978-3-662-46823-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation