nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Verifying Graph Transformation Systems with Description Logics

verfasst von : Jon Haël Brenas, Rachid Echahed, Martin Strecker

Erschienen in: Graph Transformation

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

We address the problem of verification of graph transformations featuring actions such as node merging and cloning, addition and deletion of nodes and edges, node or edge labeling and edge redirection. We introduce the considered graph rewrite systems following an algorithmic approach and then tackle their formal verification by proposing a Hoare-like weakest precondition calculus. Specifications are defined as triples of the form \(\{\texttt {Pre}\}(\texttt {R},\texttt {strategy}) \{\texttt {Post}\}\) where Pre and Post are conditions specified in a given Description Logic (DL), R is a graph rewrite system and strategy is an expression stating in which order the rules in R are to be performed. We prove that the proposed calculus is sound and characterize which DL logics are suited or not for the targeted verification tasks, according to their expressive power.

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 Equivalence and Independence in Controlled Graph-Rewriting Processes

Nächstes Kapitel OCL2AC: Automatic Translation of OCL Constraints to Graph Constraints and Application Conditions for Transformation Rules

\(h(\alpha )\) is obtained from \(\alpha \) by replacing every node name, n, of \(L\) by h(n).

Ahmetaj, S., Calvanese, D., Ortiz, M., Simkus, M.: Managing change in graph-structured data using description logics. In: Proceedings of 28th AAAI Conference on Artificial Intelligence (AAAI 2014), pp. 966–973. AAAI Press (2014)

Antoniou, G., van Harmelen, F.: Web ontology language: owl. In: Staab, S., Studer, R. (eds.) Handbook on Ontologies in Information Systems, pp. 67–92. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-24750-0_4CrossRef

Asztalos, M., Lengyel, L., Levendovszky, T.: Formal specification and analysis of functional properties of graph rewriting-based model transformation. Softw. Test. Verif. Reliabil. 23(5), 405–435 (2013)CrossRef

Baader, F.: Description logic terminology. In: The Description Logic Handbook: Theory, Implementation, and Applications, pp. 485–495 (2003)

Balbiani, P., Echahed, R., Herzig, A.: A dynamic logic for termgraph rewriting. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 59–74. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15928-2_5CrossRef

Baldan, P., Corradini, A., König, B.: A framework for the verification of infinite-state graph transformation systems. Inf. Comput. 206(7), 869–907 (2008)MathSciNetCrossRef

Baresi, L., Spoletini, P.: On the use of alloy to analyze graph transformation systems. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 306–320. Springer, Heidelberg (2006). https://doi.org/10.1007/11841883_22CrossRefMATH

Brenas, J.H., Echahed, R., Strecker, M.: A hoare-like calculus using the SROIQ\(\sigma \) logic on transformations of graphs. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 164–178. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44602-7_14CrossRef

Brenas, J.H., Echahed, R., Strecker, M.: Proving correctness of logically decorated graph rewriting systems. In: 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, pp. 14:1–14:15 (2016)

10.

Brenas, J.H., Echahed, R., Strecker, M.: On the verification of logically decorated graph transformations. CoRR, abs/1803.02776 (2018)

11.

Corradini, A., Duval, D., Echahed, R., Prost, F., Ribeiro, L.: AGREE – algebraic graph rewriting with controlled embedding. In: Parisi-Presicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 35–51. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21145-9_3CrossRefMATH

12.

Corradini, A., Heindel, T., Hermann, F., König, B.: Sesqui-pushout rewriting. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 30–45. Springer, Heidelberg (2006). https://doi.org/10.1007/11841883_4CrossRef

13.

Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990)MathSciNetCrossRef

14.

Echahed, R.: Inductively sequential term-graph rewrite systems. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 84–98. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87405-8_7CrossRefMATH

15.

Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using GROOVE. STTT 14(1), 15–40 (2012)CrossRef

16.

Habel, A., Pennemann, K.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(2), 245–296 (2009)MathSciNetCrossRef

17.

Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRef

18.

Jackson, D.: Software Abstractions. MIT Press, Cambridge (2012)

19.

König, B., Esparza, J.: Verification of graph transformation systems with context-free specifications. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 107–122. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15928-2_8CrossRefMATH

20.

Plump, D.: The graph programming language GP. In: Bozapalidis, S., Rahonis, G. (eds.) CAI 2009. LNCS, vol. 5725, pp. 99–122. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03564-7_6CrossRef

21.

Poskitt, C.M., Plump, D.: A Hoare calculus for graph programs. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 139–154. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15928-2_10CrossRefMATH

22.

Poskitt, C.M., Plump, D.: Verifying monadic second-order properties of graph programs. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 33–48. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09108-2_3CrossRefMATH

23.

Rensink, A., Distefano, D.: Abstract graph transformation. Electron. Notes Theoret. Comput. Sci. 157(1), 39–59 (2006). (In: Proceedings of 3rd International Workshop on Software Verification and Validation (SVV 2005))

24.

Rensink, A., Schmidt, Á., Varró, D.: Model checking graph transformations: a comparison of two approaches. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 226–241. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30203-2_17CrossRefMATH

25.

Virga, R.: Efficient substitution in Hoare logic expressions. Electr. Notes Theor. Comput. Sci. 41(3), 35–49 (2000)MATH

26.

Visser, E.: Stratego: a language for program transformation based on rewriting strategies system description of stratego 0.5. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 357–361. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45127-7_27CrossRefMATH

Titel: Verifying Graph Transformation Systems with Description Logics
verfasst von: Jon Haël Brenas
Rachid Echahed
Martin Strecker
Verlag: Springer International Publishing
Buch: Graph Transformation
Print ISBN: 978-3-319-92990-3

Electronic ISBN: 978-3-319-92991-0

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-92991-0_10

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"