Top

Published in:

2019 | OriginalPaper | Chapter

Product Line Verification via Modal Meta Model Checking

Authors : Tim Tegeler, Alnis Murtovi, Markus Frohme, Bernhard Steffen

Published in: From Software Engineering to Formal Methods and Tools, and Back

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Modal Meta Model Checking (M3C) is a method and tool supporting meta-level product lining and evolution that comprises both context-free system structure and modal refinement. The underlying Context-Free Modal Transition Systems (CFMTSs) can be regarded as loose specifications of meta models, and modal refinement as a way to increase the specificity of allowed domain specific languages (DSLs) by constraining the range of allowed syntax specifications. Model checking with M3C allows one to verify properties specified in a branching-time logic for all DSLs of a given level of specificity in one go. The paper illustrates the impact of M3C in an industrial setting where well-formed documents serve as contracts between a provider and its customers in two steps: it establishes CFMTS as a formalism to specify product lines of document description types (DTDs – or related formalisms like JSON schema), and it shows how M3C-based product line verification can be used to guarantee that violations of essential well-formedness constraints of a corresponding user document are detected by standard DTD-checkers. The resulting hierarchical product line verification allows Creios GmbH, a service provider for E-commerce systems to provide a wide range of tailored shop applications whose essential business rules are checked by a standard DTD-checker.

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 A Decade of Featured Transition Systems

next chapter Towards Model Checking Product Lines in the Digital Humanities: An Application to Historical Data

Our meta tooling suite CINCO [29] would, indeed, be ideally suited to generate an FTS-based development environment.

We avoid the standard notion print product here in order to avoid confusion: the products of the product line are shop applications which allow customers to configure their print goods.

It is accidental that it holds for the four products discussed in Sect. 4.1.

https://www.creios.net.

Alternatively, one can regard CFMTSs also as an extension of Context-Free Process Systems [9] to also allow may transitions.

In [19, 20] a conceptually similar structure to CFMTSs is called Systems of Procedural Automata (SPAs) to better match the terminology used in the field of automata learning.

http://fmt.isti.cnr.it/kandisti/.

Asirelli, P., ter Beek, M.H., Gnesi, S., Fantechi, A.: Formal description of variability in product families. In: 2011 15th International Software Product Line Conference, pp. 130–139, August 2011. https://doi.org/10.1109/SPLC.2011.34

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). https://doi.org/10.1007/978-3-642-16265-7_5CrossRef

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). https://doi.org/10.1007/978-3-642-21461-5_3CrossRef

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. Algebraic Methods Program. 85(2), 287–315 (2016). https://doi.org/10.1016/j.jlamp.2015.11.006MathSciNetCrossRefMATH

ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: States and events in KandISTI. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not? LNCS, vol. 11200, pp. 110–128. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-22348-9_8

Bertolino, A., Fantechi, A., Gnesi, S., Lami, G., Maccari, A.: Use case description of requirements for product lines. In: Proceedings of the International Workshop on Requirements Engineering for Product Lines 2002 - REPL 2002. Technical report: ALR2002-033, AVAYA, pp. 12–18 (2002)

Bertolino, A., Gnesi, S.: PLUTO: a test methodology for product families. In: van der Linden, F.J. (ed.) PFE 2003. LNCS, vol. 3014, pp. 181–197. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24667-1_14CrossRef

Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier Science Inc., New York (2006)MATH

Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 123–137. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0084787CrossRef

10.

Burkart, O., Steffen, B.: Pushdown processes: parallel composition and model checking. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 98–113. Springer, Heidelberg (1994). https://doi.org/10.1007/978-3-540-48654-1_9CrossRef

11.

Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. Theor. Comput. Sci. 221(1–2), 251–270 (1999). https://doi.org/10.1016/S0304-3975(99)00034-1MathSciNetCrossRefMATH

12.

Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)MATH

13.

Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y.: Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transfer 14(5), 589–612 (2012). https://doi.org/10.1007/s10009-012-0234-1CrossRef

14.

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. Software Eng. 39(8), 1069–1089 (2013). https://doi.org/10.1109/TSE.2012.86CrossRef

15.

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 ACM/IEEE International Conference on Software Engineering, ICSE 2010, vol. 1, pp. 335–344. ACM, New York (2010). https://doi.org/10.1145/1806799.1806850

16.

Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Form. Methods Syst. Des. 2(2), 121–147 (1993). https://doi.org/10.1007/BF01383878CrossRefMATH

17.

Emerson, E.A.: Model checking and the mu-calculus. In: DIMACS Series in Discrete Mathematics, pp. 185–214. American Mathematical Society (1997)

18.

Fantechi, A., Gnesi, S.: Formal modeling for product families engineering. In: 2008 12th International Software Product Line Conference, pp. 193–202, September 2008. https://doi.org/10.1109/SPLC.2008.45

19.

Frohme, M., Steffen, B.: Active mining of document type definitions. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 147–161. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_10CrossRef

20.

Frohme, M., Steffen, B.: Compositional Learning of Mutually Recursive Procedural Systems (2018, under submission)

21.

Garavel, H., Lang, F., Mounier, L.: Compositional verification in action. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 189–210. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_13CrossRef

22.

Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10 CrossRef

23.

Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186–196. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0023732CrossRef

24.

Graf, S., Steffen, B., Lüttgen, G.: Compositional minimisation of finite state systems using interface specifications. Formal Aspects Comput. 8(5), 607–616 (1996). https://doi.org/10.1007/BF01211911CrossRefMATH

25.

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

26.

Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_19CrossRef

27.

Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des. 6(1), 11–44 (1995). https://doi.org/10.1007/BF01384313CrossRefMATH

28.

Margaria, T., Steffen, B.: Simplicity as a driver for agile innovation. IEEE Comput. 43(6), 90–92 (2010). https://doi.org/10.1109/MC.2010.177CrossRef

29.

Naujokat, S., Lybecait, M., Kopetzki, D., Steffen, B.: CINCO: a simplicity-driven approach to full generation of domain-specific graphical modeling tools. STTT 20(3), 327–354 (2018). https://doi.org/10.1007/s10009-017-0453-6CrossRef

30.

O’Connor, R., Elger, P., Clarke, P.: Continuous software engineering—a microservices architecture perspective. J. Softw. Evol. Process 29 (2017). https://doi.org/10.1002/smr.1866

31.

Pohl, K., Böckle, G., van der Linden, F.J.: Software Product Line Engineering. Foundations Principles and Techniques. Springer, Heidelberg (2005). https://doi.org/10.1007/3-540-28901-1CrossRefMATH

32.

Shahin, M., Babar, M.A., Zhu, L.: Continuous integration, delivery and deployment: a systematic review on approaches, tools, challenges and practices. CoRR abs/1703.07019 (2017). http://arxiv.org/abs/1703.07019

33.

Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346–364. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54415-1_54CrossRef

34.

Steffen, B.: Generating data flow analysis algorithms from modal specifications. Sci. Comput. Program. 21(2), 115–139 (1993). https://doi.org/10.1016/0167-6423(93)90003-8CrossRefMATH

35.

Steffen, B.: Method for Incremental Synthesis of a Discrete Technical System (1998). https://patents.google.com/patent/WO1998024022A1/en

36.

Steffen, B., Gossen, F., Naujokat, S., Margaria, T.: Language-driven engineering: from general-purpose to purpose-specific languages. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science: State of the Art and Perspectives, LNCS, vol. 10000. Springer (2018). https://www.springer.com/gp/book/9783319919072

37.

Steffen, B., Murtovi, A.: M3C: modal meta model checking. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 223–241. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_15CrossRef

38.

Steffen, B., Naujokat, S.: Archimedean points: the essence for mastering change. Trans. Found. Mastering Chang. 1, 22–46 (2016). https://doi.org/10.1007/978-3-319-46508-1_3CrossRef

Title: Product Line Verification via Modal Meta Model Checking
Authors: Tim Tegeler
Alnis Murtovi
Markus Frohme
Bernhard Steffen
Publisher: Springer International Publishing
Book: From Software Engineering to Formal Methods and Tools, and Back
Print ISBN: 978-3-030-30984-8

Electronic ISBN: 978-3-030-30985-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-30985-5_19

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