Skip to main content
SpringerLink
Log in

From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL

  • Chapter
  • First Online:
Models, Algorithms, Logics and Tools

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

Abstract

Variational systems (system families) allow effective building of many custom system variants for various configurations. Lifted (family-based) verification is capable of verifying all variants of the family simultaneously, in a single run, by exploiting the similarities between the variants. These algorithms scale much better than the simple enumerative “brute-force” way. Still, the design of family-based verification algorithms greatly depends on the existence of compact variability models (state representations). Moreover, developing the corresponding family-based tools for each particular analysis is often tedious and labor intensive.

In this work, we make two contributions. First, we survey the history of development of variability models of computation that compactly represent behavior of variational systems. Second, we introduce variability abstractions that simplify variability away to achieve efficient lifted (family-based) model checking for real-time variability models. This reduces the cost of maintaining specialized family-based real-time model checkers. Real-time variability models can be model checked using the standard UPPAAL. We have implemented abstractions as syntactic source-to-source transformations on UPPAAL input files, and we illustrate the practicality of this method on a real-time case study.

Both authors are supported by The Danish Council for Independent Research under a Sapere Aude project, VARIETE.

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

Access this chapter

Log in via an institution
eBook
USD 16.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

References

  1. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993). http://dx.doi.org/10.1006/inco.1993.1024

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). http://dx.doi.org/10.1016/0304-3975(94)90010-8

    Article  MathSciNet  MATH  Google Scholar 

  3. Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  4. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30080-9_7

    Chapter  Google Scholar 

  5. 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). doi:10.1007/978-3-642-24372-1_20

    Chapter  Google Scholar 

  6. Bodden, E., Tolêdo, T., Ribeiro, M., Brabrand, C., Borba, P., Mezini, M.: SPLLIFT: statically analyzing software product lines in minutes instead of years. In: ACM SIGPLAN Conference on PLDI 2013, pp. 355–364 (2013)

    Google Scholar 

  7. Brabrand, C., Ribeiro, M., Tolêdo, T., Winther, J., Borba, P.: Intraprocedural dataflow analysis for software product lines. In: Leavens, G.T., Chiba, S., Tanter, É. (eds.) Transactions on Aspect-Oriented Software Development X. LNCS, vol. 7800, pp. 73–108. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36964-3_3

    Chapter  Google Scholar 

  8. Čerāns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification - Theory and tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253–267. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_21

    Chapter  Google Scholar 

  9. Classen, A., Boucher, Q., Heymans, P.: A text-based approach to feature modelling: syntax and semantics of TVL. Sci. Comput. Program. 76(12), 1130–1143 (2011). http://dx.doi.org/10.1016/j.scico.2010.10.005

    Article  Google Scholar 

  10. Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.: Model checking software product lines with SNIP. STTT 14(5), 589–612 (2012). http://dx.doi.org/10.1007/s10009-012-0234-1

    Article  Google Scholar 

  11. Classen, A., Cordy, M., Schobbens, P., Heymans, P., Legay, A., Raskin, J.: 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). http://doi.ieeecomputersociety.org/10.1109/TSE.2012.86

    Article  Google Scholar 

  12. Cordy, M., Classen, A., Heymans, P., Schobbens, P., Legay, A.: Provelines: a product line of verifiers for software product lines. In: 17th International Software Product Line Conference Co-located Workshops, SPLC 2013 Workshops, pp. 141–146. ACM (2013). http://doi.acm.org/10.1145/2499777.2499781

  13. Cordy, M., Schobbens, P., Heymans, P., Legay, A.: Behavioural modelling and verification of real-time software product lines. In: 16th International Software Product Line Conference, SPLC 2012, vol. 1, pp. 66–75. ACM (2012). http://doi.acm.org/10.1145/2362536.2362549

  14. Czarnecki, K., Antkiewicz, M.: Mapping features to models: a template approach based on superimposed variants. In: Glück, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol. 3676, pp. 422–437. Springer, Heidelberg (2005). doi:10.1007/11561347_28

    Chapter  Google Scholar 

  15. Dimovski, A., Brabrand, C., Wąsowski, A.: Variability abstractions: trading precision for speed in family-based analyses. In: 29th European Conference on Object-Oriented Programming ECOOP 2015. LIPIcs, vol. 37, pp. 247–270. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)

    Google Scholar 

  16. Dimovski, A.S.: Program verification using symbolic game semantics. Theor. Comput. Sci. 560, 364–379 (2014). http://dx.doi.org/10.1016/j.tcs.2014.01.016

    Article  MathSciNet  MATH  Google Scholar 

  17. Dimovski, A.S.: Symbolic game semantics for model checking program families. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 19–37. Springer, Cham (2016). doi:10.1007/978-3-319-32582-8_2

    Chapter  Google Scholar 

  18. 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). doi:10.1007/978-3-319-23404-5_18

    Chapter  Google Scholar 

  19. Dimovski, A.S., Al-Sibahi, A.S., Brabrand, C., Wasowski, A.: Efficient family-based model checking via variability abstractions. In: STTT, pp. 1–19 (2016)

    Google Scholar 

  20. Dimovski, A.S., Brabrand, C., Wąsowski, A.: Finding suitable variability abstractions for family-based analysis. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 217–234. Springer, Cham (2016). doi:10.1007/978-3-319-48989-6_14

    Chapter  Google Scholar 

  21. Dimovski, A.S., Wąsowski, A.: Variability-specific abstraction refinement for family-based model checking. In: Huisman, M., Rubin, J. (eds.) FASE 2017. LNCS, vol. 10202, pp. 406–423. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54494-5_24

    Chapter  Google Scholar 

  22. Gazzillo, P., Grimm, R.: SuperC: parsing all of C by taming the preprocessor. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, pp. 323–334. ACM (2012). http://doi.acm.org/10.1145/2254064.2254103

  23. Iosif-Lazar, A.F., Melo, J., Dimovski, A.S., Brabrand, C., Wasowski, A.: Effective analysis of C programs by rewriting variability. In: The Art, Science, and Engineering of Programming, Programming 2017, vol. 1, no. 1, pp. 1–25 (2017)

    Google Scholar 

  24. Kästner, C., Apel, S., Thüm, T., Saake, G.: Type checking annotation-based product lines. ACM Trans. Softw. Eng. Methodol. 21(3), 14 (2012)

    Article  Google Scholar 

  25. Kästner, C., Giarrusso, P.G., Rendel, T., Erdweg, S., Ostermann, K., Berger, T.: Variability-aware parsing in the presence of lexical macros and conditional compilation. In: OOPSLA 2011, pp. 805–824. ACM, Portland (2011)

    Google Scholar 

  26. Larsen, K.G.: Context-dependent bisimulation between processes. Ph.D. thesis, University of Edinburgh, UK, May 1986

    Google Scholar 

  27. Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71316-6_6

    Chapter  Google Scholar 

  28. Larsen, K.G., Nyman, U., Wasowski, A.: Modeling software product lines using color-blind transition systems. STTT 9(5–6), 471–487 (2007)

    Article  Google Scholar 

  29. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1–2), 134–152 (1997). http://dx.doi.org/10.1007/s100090050010

    Article  MATH  Google Scholar 

  30. Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS 1988), pp. 203–210. IEEE Computer Society (1988). http://dx.doi.org/10.1109/LICS.1988.5119

  31. Midtgaard, J., Dimovski, A.S., Brabrand, C., Wąsowski, A.: Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program. 105, 145–170 (2015). http://dx.doi.org/10.1016/j.scico.2015.04.005

    Article  Google Scholar 

  32. Minsky, M.: Computation: Finite and Infinite Machines. Prentice Hall, Princeton (1967)

    MATH  Google Scholar 

  33. von Rhein, A., Thüm, T., Schaefer, I., Liebig, J., Apel, S.: Variability encoding: from compile-time to load-time variability. J. Log. Algebr. Meth. Program. 85(1), 125–145 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  34. Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Formal Description Techniques VII, Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques, IFIP Conference Proceedings, vol. 6, pp. 243–258. Chapman & Hall (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science, IT University of Copenhagen, Copenhagen, Denmark

    Aleksandar S. Dimovski & Andrzej Wąsowski

Authors
  1. Aleksandar S. Dimovski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrzej Wąsowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Aleksandar S. Dimovski .

Editor information

Editors and Affiliations

  1. Reykjavik University, Reykjavik, Iceland

    Luca Aceto

  2. Aalborg University, Aalborg, Denmark

    Giorgio Bacci

  3. Aalborg University, Aalborg, Denmark

    Giovanni Bacci

  4. Reykjavík University, Reykjavik, Iceland

    Anna Ingólfsdóttir

  5. Inria Campus Beaulieu, Rennes, France

    Axel Legay

  6. Aalborg University, Aalborg, Denmark

    Radu Mardare

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Dimovski, A.S., Wąsowski, A. (2017). From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL . In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds) Models, Algorithms, Logics and Tools. Lecture Notes in Computer Science(), vol 10460. Springer, Cham. https://doi.org/10.1007/978-3-319-63121-9_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63121-9_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63120-2

  • Online ISBN: 978-3-319-63121-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation