nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

30.06.2018 | FASE 2017

Automated reasoning for attributed graph properties

verfasst von: Sven Schneider, Leen Lambers, Fernando Orejas

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2018

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Graphs are ubiquitous in computer science. Moreover, in various application fields, graphs are equipped with attributes to express additional information such as names of entities or weights of relationships. Due to the pervasiveness of attributed graphs, it is highly important to have the means to express properties on attributed graphs to strengthen modeling capabilities and to enable analysis. Firstly, we introduce a new logic of attributed graph properties, where the graph part and attribution part are neatly separated. The graph part is equivalent to first-order logic on graphs as introduced by Courcelle. It employs graph morphisms to allow the specification of complex graph patterns. The attribution part is added to this graph part by reverting to the symbolic approach to graph attribution, where attributes are represented symbolically by variables whose possible values are specified by a set of constraints making use of algebraic specifications. Secondly, we extend our refutationally complete tableau-based reasoning method as well as our symbolic model generation approach for graph properties to attributed graph properties. Due to the new logic mentioned above, neatly separating the graph and attribution parts, and the categorical constructions employed only on a more abstract level, we can leave the graph part of the algorithms seemingly unchanged. For the integration of the attribution part into the algorithms, we use an oracle, allowing for flexible adoption of different available SMT solvers in the actual implementation. Finally, our automated reasoning approach for attributed graph properties is implemented in the tool AutoGraph integrating in particular the SMT solver Z3 for the attribute part of the properties. We motivate and illustrate our work with a particular application scenario on graph database query validation.

Vorheriger Artikel Learning probabilistic models for model checking: an evolutionary approach and an empirical study

Nächster Artikel Slicing from formal semantics: Chisel—a tool for generic program slicing

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

Nur mit Berechtigung zugänglich

Firstly, the algebraic specification used is given by \((\Sigma _{A_2}, EQ )\) where \(\Sigma _{A_2}\) is the signature with variables obtained for the attribution \(A_2\) of \(G_2^{ sa }\) and the signature \(\Sigma \) from \( SP \) as in Definition 10. Secondly, \(f_{AX}: AX _1\rightarrow AX _2\) is a member of \(\mathcal {V}_{\Sigma _{A_1},\Sigma _{A_2}} \) according to Definition 4.

The empty conjunction \(\wedge \emptyset \) is the base case of the inductive definition.

Formally, the family is a map that assigns one triple to each \(i\in I'\).

Intuitively, a triple \(\langle T_i,j,c_i\rangle \) is either generated by the initialization rule or is generated by the nesting rule and \(T_i\) is a tableau for a condition \(c_i\) that is the inner condition of some literal \(\ell =\exists (m,c_i)\) that is in a leaf node of the parent tableau \(T_j\) that is assigned to index j in \( NT \).

Abiteboul, S., Hull, R., Vianu, V. (eds.): Foundations of Databases: The Logical Level, 1st edn. Addison-Wesley Longman Publishing Co., Inc., Boston, MA (1995)

Angles, R., Arenas, M., Barceló, P., Hogan, A., Reutter, J.L., Vrgoc, D.: Foundations of modern graph query languages. CoRR, abs/1610.06264 (2016)

Angles, R., Gutierrez, C.: Survey of graph database models. ACM Comput. Surv. 40(1), 1:1–1:39 (2008)CrossRef

Bak, K., Diskin, Z., Antkiewicz, M., Czarnecki, K., Wasowski, A.: Clafer: unifying class and feature modeling. Softw. Syst. Model. 15(3), 811–845 (2016)CrossRef

Baudry, B.: Testing model transformations: a case for test generation from input domain models. In: Model-Driven Engineering for Distributed Real-Time Systems, Chap. 3, pp. 43–72. Wiley (2013). https://doi.org/10.1002/9781118558096.ch3 CrossRef

Beyhl, T., Blouin, D., Giese, H., Lambers, L.: On the operationalization of graph queries with generalized discrimination networks. In: Echahed and Minas [12], pp. 170–186CrossRef

Blanco, R., Tuya, J.: A test model for graph database applications: an MDA-based approach. In: Vos Tanja E.J. Eldh, S., Prasetya, W. (eds.) Proceedings of the 6th International Workshop on Automating Test Case Design, Selection and Evaluation, A-TEST 2015, Bergamo, Italy, August 30–31, 2015, pp. 8–15. ACM (2015)

Codd, E.F.: A relational model of data for large shared data banks. Commun. ACM 13(6), 377–387 (1970)CrossRef

Courcelle, B.: The expression of graph properties and graph transformations in monadic second-order logic. In: Rozenberg [44], pp. 313–400CrossRef

10.

Daniel, G., Sunyé, G., Cabot, J.: Umltographdb: mapping conceptual schemas to graph databases. In: Comyn-Wattiau, I., Tanaka, K., Song, I.-Y., Yamamoto, S., Saeki, M. (eds.) Conceptual Modeling—35th International Conference, volume 9974 of Lecture Notes in Computer Science, pp. 430–444 (2016)CrossRef

11.

Deckwerth, F.: Static verification techniques for attributed graph transformations. Ph.D. thesis, Darmstadt University of Technology, Germany (2017)

12.

Echahed, R., Minas, M. (eds.): Graph Transformation—9th International Conference, ICGT 2016, in Memory of Hartmut Ehrig, Held as Part of STAF 2016, Vienna, Austria, July 5–6, 2016, Proceedings, volume 9761 of Lecture Notes in Computer Science. Springer (2016)

13.

Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer, Berlin (2006)MATH

14.

Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: \(\cal{M}\)-adhesive transformation systems with nested application conditions. Part 2: embedding, critical pairs and local confluence. Fundam. Inform. 118(1–2), 35–63 (2012). https://doi.org/10.3233/FI-2012-705 MathSciNetCrossRefMATH

15.

Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G., (eds.): Graph Transformations, 4th International Conference, ICGT 2008, Leicester, United Kingdom, September 7–13, 2008. Proceedings, volume 5214 of Lecture Notes in Computer Science. Springer (2008)

16.

Ehrig, H., Mahr, B.: Fundamentals of algebraic specification 1: equations und initial semantics. In: EATCS Monographs on Theoretical Computer Science, vol. 6. Springer, Heidelberg (1985). https://doi.org/10.1007/978-3-642-69962-7 CrossRefMATH

17.

Giese, H., König, B. (eds.): Graph Transformation—7th International Conference, ICGT 2014, Held as Part of STAF 2014, York, UK, July 22–24, 2014. Proceedings, volume 8571 of Lecture Notes in Computer Science. Springer (2014)

18.

Gogolla, M., Hilken, F.: Model validation and verification options in a contemporary UML and OCL analysis tool. In: Oberweis, A., Reussner, R.H., (eds.) Modellierung 2016, 2.-4. März 2016, Karlsruhe, volume 254 of LNI, pp. 205–220. GI (2016)

19.

González, C.A., Cabot, J.: Test data generation for model transformations combining partition and constraint analysis. In: Ruscio, D.D., Varró, D. (eds.) Theory and Practice of Model Transformations—7th International Conference, ICMT 2014, Held as Part of STAF 2014, York, UK, July 21–22, 2014. Proceedings, volume 8568 of Lecture Notes in Computer Science, pp. 25–41. Springer (2014)

20.

Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Inform. 26(3/4), 287–313 (1996)MathSciNetMATH

21.

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

22.

Hähnle, R.: Tableaux and related methods. In Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 100–178. Elsevier and MIT Press (2001)

23.

Heckel, R., Wagner, A.: Ensuring consistency of conditional graph rewriting—a constructive approach. Electr. Notes Theor. Comput. Sci. 2, 118–126 (1995)CrossRef

24.

Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: Whittle, J., Clark, T., Kühne, T. (eds.) Model Driven Engineering Languages and Systems, 14th International Conference, MODELS 2011, Wellington, New Zealand, October 16–21, 2011. Proceedings, volume 6981 of Lecture Notes in Computer Science, pp. 653–667. Springer (2011)

25.

Jackson, E.K., Sztipanovits, J.: Constructive techniques for meta- and model-level reasoning. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) Model Driven Engineering Languages and Systems, 10th International Conference, MoDELS 2007, Nashville, USA, September 30–October 5, 2007, Proceedings, volume 4735 of Lecture Notes in Computer Science, pp. 405–419. Springer (2007)

26.

Krause, C., Johannsen, D., Deeb, R., Sattler, K.-U., Knacker, D., Niadzelka, A.: An SQL-based query language and engine for graph pattern matching. In: Echahed and Minas [12], pp. 153–169CrossRef

27.

Lambers, L., Orejas, F.: Tableau-based reasoning for graph properties. In: Giese and König [17], pp. 17–32MATH

28.

Microsoft Corporation. Z3. https://github.com/Z3Prover/z3. Accessed 19 Sept 2017

29.

Milicevic, A., Near, J.P., Eunsuk, K., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: Bertolino, A., Canfora, G., Elbaum, S.G. (eds.) 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16–24, 2015, Volume 1, pp. 609–619. IEEE Computer Society (2015)

30.

Mougenot, A., Darrasse, A., Blanc, X., Soria, M.: Uniform random generation of huge metamodel instances. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) Model Driven Architecture—Foundations and Applications, 5th European Conference, ECMDA-FA 2009, Enschede, The Netherlands, June 23–26, 2009. Proceedings, volume 5562 of Lecture Notes in Computer Science, pp. 130–145. Springer (2009)

31.

Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) 35th International Conference on Software Engineering, ICSE ’13, San Francisco, CA, USA, May 18–26, 2013, pp. 232–241. IEEE Computer Society (2013)

32.

Orejas, F.: Attributed graph constraints. In: Ehrig et al. [15], pp. 274–288

33.

Orejas, F., Ehrig, H., Prange, U.: A logic of graph constraints. In: Fiadeiro, J.L., Inverardi, P. (eds.) Fundamental Approaches to Software Engineering, 11th International Conference, FASE 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4961 of Lecture Notes in Computer Science, pp. 179–198. Springer (2008)

34.

Orejas, F., Ehrig, H., Prange, U.: Reasoning with graph constraints. Formal Asp. Comput. 22(3–4), 385–422 (2010)CrossRef

35.

Orejas, F., Lambers, L.: Symbolic attributed graphs for attributed graph transformation. ECEASST 30, (2010). https://doi.org/10.1016/j.jsc.2010.09.009 MathSciNetCrossRef

36.

Orejas, F., Lambers, L.: Lazy graph transformation. Fundam. Inform. 118(1–2), 65–96 (2012)MathSciNetMATH

37.

Pennemann, K.-H.: An algorithm for approximating the satisfiability problem of high-level conditions. Electr. Notes Theor. Comput. Sci. 213(1), 75–94 (2008)CrossRef

38.

Pennemann, K.-H.: Resolution-like theorem proving for high-level conditions. In: Ehrig et al. [15], pp. 289–304

39.

Pennemann, K.-H.: Development of correct graph transformation systems, Ph.D. Thesis. Dept. Informatik, Univ. Oldenburg (2009)

40.

Poskitt, C.M., Plump, D.: Verifying monadic second-order properties of graph programs. In: Giese and König [17], pp. 33–48MATH

41.

Radke, H.: HR* graph conditions between counting monadic second-order and second-order graph formulas. ECEASST 61, (2013). https://doi.org/10.14279/tuj.eceasst.61.831.831

42.

Radke, H., Arendt, T., Becker, J.S., Habel, A., Taentzer, G.: Translating essential OCL invariants to nested graph constraints focusing on set operations. In: Parisi-Presicce, F., Westfechtel, B. (eds.) Graph Transformation—8th International Conference, ICGT 2015, Held as Part of STAF 2015, L’Aquila, Italy, July 21–23, 2015. Proceedings, volume 9151 of Lecture Notes in Computer Science, pp. 155–170. Springer (2015)

43.

Rensink, A.: Representing first-order logic using graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) Graph Transformations, Second International Conference, ICGT 2004, Rome, Italy, September 28–October 2, 2004, Proceedings, volume 3256 of Lecture Notes in Computer Science, pp. 319–335. Springer (2004)

44.

Rozenberg, G. (ed.).: Handbook of graph grammars and computing by graph transformations, vol. 1: foundations. World Scientific (1997). https://doi.org/10.1142/3303 CrossRef

45.

Salay, R., Chechik, M.: A generalized formal framework for partial modeling. In: Egyed, A., Schaefer, I. (eds.) Fundamental Approaches to Software Engineering—18th International Conference, FASE 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings, volume 9033 of Lecture Notes in Computer Science, pp. 133–148. Springer (2015)

46.

Schneider, S., Lambers, L., Orejas, F.: Symbolic model generation for graph properties. In: Huisman, M., Rubin, J. (eds). Fundamental Approaches to Software Engineering—20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings, volume 10202 of Lecture Notes in Computer Science, pp. 226–243. Springer (2017)

47.

Schneider, S., Lambers, L., Orejas, F.: Symbolic model generation for graph properties (extended version). Number 115 in Technische Berichte des Hasso-Plattner-Instituts fr Softwaresystemtechnik an der Universität Potsdam. Universitätsverlag Potsdam, Hasso Plattner Institute (Germany, Potsdam), 1 edition, 2 (2017)

48.

Schweikardt, N., Schwentick, T., Segoufin, L.: Algorithms and Theory of Computation Handbook. Chapter Database Theory: Query Languages, vol. 19, pp. 1–34. Chapman & Hall/CRC, Boca Raton (2010)

49.

Semeráth, O., Varró, D.: Graph constraint evaluation over partial models by constraint rewriting. In: Guerra, E., van den Brand, M. (eds.) Theory and Practice of Model Transformation—10th International Conference, ICMT 2017, Held as Part of STAF 2017, Marburg, Germany, July 17–18, 2017, Proceedings, volume 10374 of Lecture Notes in Computer Science, pp. 138–154. Springer (2017)

50.

Semeráth, O., Vörös, A., Varró, D.: Iterative and incremental model generation by logic solvers. In: Stevens, P., Wasowski, A. (eds.) Fundamental Approaches to Software Engineering—19th International Conference, FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings, volume 9633 of Lecture Notes in Computer Science, pp. 87–103. Springer (2016)CrossRef

51.

The Linked Data Benchmark Council (LDBC). Social network benchmark. https://github.com/ldbc/ldbc_snb_docs. Accessed: 21 Aug 2017

52.

The World Wide Web Consortium (W3C). W3c xml schema definition language (xsd) 1.1 part 1: Structures (2012)

53.

Wood, P.T.: Query languages for graph databases. SIGMOD Rec. 41(1), 50–60 (2012)CrossRef

Titel: Automated reasoning for attributed graph properties
verfasst von: Sven Schneider
Leen Lambers
Fernando Orejas
Publikationsdatum: 30.06.2018
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 6/2018
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-018-0496-3

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"

Weitere Artikel der Ausgabe 6/2018

Slicing ATL model transformations for scalable deductive verification and fault localization

Slicing from formal semantics: Chisel—a tool for generic program slicing

Learning probabilistic models for model checking: an evolutionary approach and an empirical study

Tactical contract composition for hybrid system component verification

Software quality tools and techniques presented in FASE’17

Automated workarounds from Java program specifications based on SAT solving

Premium Partner