Top

Published in:

2017 | OriginalPaper | Chapter

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

Authors : Aleksandar S. Dimovski, Andrzej Wąsowski

Published in: Models, Algorithms, Logics and Tools

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Synchronous Interfaces and Assume/Guarantee Contracts

next chapter Firm Deadline Checking of Safety-Critical Java Applications with Statistical Model Checking

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 MathSciNetCrossRefMATH

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 MathSciNetCrossRefMATH

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

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 CrossRef

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 CrossRef

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)

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 CrossRef

Č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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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 CrossRef

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)

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 MathSciNetCrossRefMATH

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 CrossRef

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 CrossRef

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)

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 CrossRef

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 CrossRef

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)

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)CrossRef

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)

26.

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

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 CrossRef

28.

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

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 CrossRefMATH

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 CrossRef

32.

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

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)MathSciNetCrossRefMATH

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)

Title: From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL
Authors: Aleksandar S. Dimovski
Andrzej Wąsowski
Publisher: Springer International Publishing
Book: Models, Algorithms, Logics and Tools
Print ISBN: 978-3-319-63120-2

Electronic ISBN: 978-3-319-63121-9

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-63121-9_13

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner