nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

M3C: Modal Meta Model Checking

verfasst von : Bernhard Steffen, Alnis Murtovi

Erschienen in: Formal Methods for Industrial Critical Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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 can be regarded as loose specifications of meta models, and modal refinement as a way to increase the specificity of allowed 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, which is illustrated by looking at variations of an elementary programming language. Technically, M3C is based on second-order model checking which determines how procedure calls affect the validity of the properties of interest. The inherent compositionality of the second-order approach leads to a runtime complexity linear in the size of the procedural system representation, whose corresponding transition systems typically have infinitely many states. In fact, second-order model checking can be regarded as a means to tame state explosion via ‘procedural abstraction’, a technique which may well be beneficial also for regular (recursion-free) systems.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel A Note on Refinement in Hierarchical Transition Systems

Nächstes Kapitel Wholly!: A Build System For The Modern Software Stack

We are focusing here on the alternation-free mu-calculus.

Such properties are called rigid archimedean points in [20].

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

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

The figures generated by our tool.

For readability, in comparison to the specification in Sect. 2, we factored the constant-, variable- and procedure-declarations out here as own PMTSs.

The reader is invited to consider other refinement options. Please note, due to unrolling there are infinitely many options!

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

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

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

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

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

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

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)

Frohme, M., Steffen, B.: Compositional learning of mutually recursive procedural systems (2018, under submission)

10.

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)

11.

Gössler, G., Graf, S., Majster-Cederbaum, M., Martens, M., Sifakis, J.: An approach to modelling and verification of component based systems. In: van Leeuwen, J., Italiano, G.F., van der Hoek, W., Meinel, C., Sack, H., Plášil, F. (eds.) SOFSEM 2007. LNCS, vol. 4362, pp. 295–308. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69507-3_24CrossRefMATH

12.

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_10CrossRef

13.

Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Computer-Aided Verification, Proceedings of a DIMACS Workshop 1990, New Brunswick, New Jersey, USA, 18–21 June 1990, pp. 57–74 (1990)

14.

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

15.

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

16.

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

17.

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

18.

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

19.

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. LNCS, vol. 10000, pp. 311–344. Springer, Cham (2018)

20.

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

21.

Wirth, N.: Compilerbau - Eine Einführung. Teubner (1977)

Titel: M3C: Modal Meta Model Checking
verfasst von: Bernhard Steffen
Alnis Murtovi
Verlag: Springer International Publishing
Buch: Formal Methods for Industrial Critical Systems
Print ISBN: 978-3-030-00243-5

Electronic ISBN: 978-3-030-00244-2

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-00244-2_15

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner