×

zbMATH — the first resource for mathematics

Theorem proving graph grammars with attributes and negative application conditions. (English) Zbl 1371.68139
Summary: Graph grammars may be used to formally describe computational systems, modeling the states as graphs and the possible state changes as rules (whose left- and right-hand sides are graphs). The behavior of the system is defined by the application of these rules to the state-graphs. From a practical point of view, the extension of rules to enable description of extra conditions that must be satisfied upon rule application is highly desirable. An example is the specification of negative application conditions, or NACs, that describe situations that prevent the application of a rule. This extension of the basic formalism enhances the expressiveness of rules, generally allowing simpler specifications. Another extension that is fundamental for practical applications is the possibility to use data types, like natural numbers, lists, etc., as attributes of graphical elements (vertices and edges). Attributed graph grammars are well-investigated and used. However, there is a lack of verification techniques for this kind of grammar mainly due to the fact that data types are typically infinite domains, and thus techniques like model checking can not be used directly (without abstraction constructions). The present work provides a theoretical foundation for theorem proving graph grammars with negative application conditions and attributes. This is achieved by generating an event-B model from a graph grammar. Event-B models are composed by sets and axioms to define types, and by states and events to describe behavior. After constructing the event-B model that is semantically equivalent to a graph grammar, properties about reachable states may be proven using the various theorem provers available for event-B in the Rodin platform. This strategy allows the verification of systems with infinite-state spaces without using any kind of approximation.
MSC:
68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Promela language reference
[2] A heuristic solution for model checking graph transformation systems, Appl. Soft Comput., 24, 169-180, (2014)
[3] Abrial, J. R., The B-book: assigning programs to meanings, (2005), Cambridge University Press · Zbl 0915.68015
[4] Abrial, Jean-Raymond, Modeling in event-B: system and software engineering, (2010), Cambridge University Press · Zbl 1213.68214
[5] Abrial, Jean-Raymond; Hallerstede, Stefan, Refinement, decomposition, and instantiation of discrete models: application to event-B, Fund. Inform., 77, 1-2, 1-28, (2007) · Zbl 1118.68392
[6] Abrial, Jean-Raymond; Butler, Michael; Hallerstede, Stefan; Hoang, Thai Son; Mehta, Farhad; Voisin, Laurent, Rodin: an open toolset for modelling and reasoning in event-B, Int. J. Softw. Tools Technol. Transf., 12, 6, 447-466, (2010)
[7] Arendt, Thorsten; Biermann, Enrico; Jurack, Stefan; Krause, Christian; Taentzer, Gabriele, Henshin: advanced concepts and tools for in-place EMF model transformations, (13th International Conference on Model Driven Engineering Languages and Systems: Part I, MODELS’10, (2010), Springer-Verlag), 121-135
[8] Azab, Karl; Habel, Annegret; Pennemann, Karl-Heinz; Zuckschwerdt, Christian, Enforce: a system for ensuring formal correctness of high-level programs, Electron. Commun. EASST, 1, (2006)
[9] Back, Ralph-Johan; Sere, Kaisa, Stepwise refinement of action systems, (van de Snepscheut, Jan L. A., International Conference on Mathematics of Program Construction, (1989), Springer-Verlag), 115-138
[10] Baldan, Paolo; Corradini, Andrea; König, Barbara, A framework for the verification of infinite-state graph transformation systems, Inform. and Comput., 206, 7, 869-907, (2008) · Zbl 1153.68034
[11] Baresi, Luciano; Spoletini, Paola, On the use of alloy to analyze graph transformation systems, (Third International Conference on Graph Transformations, ICGT’06, (2006), Springer-Verlag), 306-320 · Zbl 1156.68340
[12] Saddek, Bensalem; Vijay, Ganesh; Yassine, Lakhnech; Owre, César Mu; Rueß, Sam; Rushby, Harald; Rusu, John; Saïdi, Vlad; Shankar, Hassen; Singerman Eli, N.; Ashish, Tiwari, An overview of SAL, (Holloway, C. Michael, Fifth NASA Langley Formal Methods Workshop, (2000)), 187-196
[13] Bertot, Yves; Castéran, Pierre, Interactive theorem proving and program development: coq’art: the calculus of inductive constructions, Texts in Theoretical Computer Science, (2004), Springer-Verlag · Zbl 1069.68095
[14] Boolos, George S., On second-order logic, J. Philos., 72, 16, 509-527, (1975)
[15] Born, Kristopher; Arendt, Thorsten; Heß, Florian; Taentzer, Gabriele, Analyzing conflicts and dependencies of rule-based transformations, (Egyed, Alexander; Schaefer, Ina, 18th International Conference on Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 9033, (2015), Springer-Verlag), 165-168
[16] Andrea Corradini, Ugo Montanari, Francesca Rossi, Hartmut Ehrig, Reiko Heckel, Michael Löwe, Algebraic approaches to graph transformation - part I: basic concepts and double pushout approach, in: [71].
[17] Corradini, Andrea; Duval, Dominique; Echahed, Rachid; Prost, Frédéric; Ribeiro, Leila, AGREE - algebraic graph rewriting with controlled embedding, (8th International Conference on Graph Transformation, Lecture Notes in Computer Science, vol. 9151, (2015), Springer-Verlag), 35-51 · Zbl 1321.68327
[18] Bruno Courcelle, The expression of graph properties and graph transformations in monadic second-order logic, in: [71]. · Zbl 0883.03004
[19] Csertan, G.; Huszerl, G.; Majzik, I.; Pap, Z.; Pataricza, A.; Varr’o, D’aniel, VIATRA - visual automated transformations for formal verification and validation of UML models, (17th IEEE International Conference on Automated Software Engineering, (2002)), 267-270
[20] da Costa, Simone André, Relational approach of graph grammars, (2010), UFRGS Brazil, Ph.D. thesis
[21] da Costa, Simone André; Ribeiro, Leila, Formal verification of graph grammars using mathematical induction, Electron. Notes Theor. Comput. Sci., 240, 43-60, (2009) · Zbl 1347.68243
[22] da Costa, Simone André; Ribeiro, Leila, Verification of graph grammars using a logical approach, Sci. Comput. Program., 77, 4, 480-504, (2012) · Zbl 1243.68211
[23] da Costa Cavalheiro, Simone André; Foss, Luciana; Ribeiro, Leila, Specification patterns for properties over reachable states of graph grammars, (Gheyi, Rohit; Naumann, David A., 15th Brazilian Symposium on Formal Methods: Foundations and Applications, Lecture Notes in Computer Science, vol. 7498, (2012), Springer-Verlag), 83-98 · Zbl 1372.68180
[24] DEPLOY, Event-B and the rodin platform, (2008), Rodin Development is supported by European Union ICT Projects DEPLOY (2008 to 2012) and RODIN (2004 to 2007)
[25] Dotti, Fernando Luís; Foss, Luciana; Ribeiro, Leila; dos Santos, Osmar Marchi, Verification of distributed object-based systems, (6th International Conference on Formal Methods for Open Object-Based Distributed Systems, (2003)), 261-275 · Zbl 1253.68059
[26] Duval, Dominique; Echahed, Rachid; Prost, Frédéric; Ribeiro, Leila, Transformation of attributed structures with cloning, (17th International Conference on Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 8411, (2014), Springer-Verlag), 310-324
[27] (Ehrig, H.; Engels, G.; Kreowski, H.-J.; Rozenberg, G., Handbook of Graph Grammars and Computing by Graph Transformation, vol. 2: Applications, Languages, and Tools, (1999), World Scientific Publishing Co., Inc.) · Zbl 0998.68001
[28] Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G., Fundamentals of algebraic graph transformation, (2006), Springer-Verlag · Zbl 1095.68047
[29] Ehrig, Hartmut, Introduction to the algebraic theory of graph grammars (-survey), (Claus, Volker; Ehrig, Hartmut; Rozenberg, Grzegorz, International Workshop on Graph-Grammars and Their Application to Computer Science and Biology, Lecture Notes in Computer Science, vol. 73, (1979), Springer-Verlag), 1-69 · Zbl 0407.68072
[30] Hartmut Ehrig, Reiko Heckel, Martin Korff, Michael Löwe, Leila Ribeiro, Annika Wagner, Andrea Corradini, Algebraic approaches to graph transformation - part II: single pushout approach and comparison with double pushout approach, in: [71].
[31] Ehrig, Hartmut; Ehrig, Karsten; Prange, Ulrike; Taentzer, Gabriele, Fundamental theory for typed attributed graphs and graph transformation based on adhesive HLR categories, Fundam. Inform., 74, 1, 31-61, (2006) · Zbl 1106.68055
[32] Ermel, C.; Rudolf, M.; Taentzer, G., The AGG approach: language and environment, (Ehrig, H.; Engels, G.; Kreowski, H.-J.; Rozenberg, G., Handbook of Graph Grammars and Computing by Graph Transformation, vol. 2: Applications, Languages, and Tools, (1999), World Scientific Publishing Co., Inc.)
[33] Ermel, Claudia; Biermann, Enrico; Schmidt, Johann; Warning, Angeline, Visual modeling of controlled EMF model transformation using HENSHIN, Electron. Commun. EASST, 32, (2010)
[34] Galvão, Ismênia; Zambon, Eduardo; Rensink, Arend; Wevers, Lesley; Aksit, Mehmet, Knowledge-based graph exploration analysis, (Schürr, Andy; Varró, Dániel; Varró, Gergely, 4th International Symposium on Applications of Graph Transformations with Industrial Relevance, Lecture Notes in Computer Science, vol. 7233, (2011), Springer-Verlag), 105-120
[35] Garavel, Hubert; Lang, Frédéric; Mateescu, Radu; Serwe, Wendelin, CADP 2011: a toolbox for the construction and analysis of distributed processes, Int. J. Softw. Tools Technol. Transf., 15, 2, 89-107, (2013)
[36] Ghamarian, Amir Hossein; de Mol, Maarten; Rensink, Arend; Zambon, Eduardo; Zimakova, Maria, Modelling and analysis using GROOVE, Int. J. Softw. Tools Technol. Transf., 14, 1, 15-40, (2012)
[37] Girard, Jean-Yves, Linear logic, Theoret. Comput. Sci., 50, 1, 1-101, (1987) · Zbl 0625.03037
[38] Golas, Ulrike, A general attribution concept for models in \(\mathcal{M}\)-adhesive transformation systems, (6th International Conference on Graph Transformations, Lecture Notes in Computer Science, vol. 7562, (2012), Springer-Verlag), 187-202 · Zbl 1367.68133
[39] Groote, J. F.; Keiren, J.; Mathijssen, A.; Ploeger, B.; Stappers, F.; Tankink, C.; Usenko, Y.; Weerdenburg, M. van; Wesselink, W.; Willemse, T.; van der Wulp, J., The mcrl2 toolset, (International Workshop on Advanced Software Development Tools and Techniques, (2008))
[40] Habel, Annegret; Pennemann, Karl-Heinz, Correctness of high-level transformation systems relative to nested conditions, Math. Structures Comput. Sci., 19, 4, 245-296, (2009) · Zbl 1168.68022
[41] Habel, Annegret; Plump, Detlef, Relabelling in graph transformation, (First International Conference on Graph Transformation, Lecture Notes in Computer Science, vol. 2505, (2002), Springer-Verlag), 135-147 · Zbl 1028.68071
[42] Habel, Annegret; Heckel, Reiko; Taentzer, Gabriele, Graph grammars with negative application conditions, Fund. Inform., 26, 3-4, 287-313, (1996) · Zbl 0854.68055
[43] Habel, Annegret; Pennemann, Karl-Heinz; Rensink, Arend, Weakest preconditions for high-level programs, (Corradini, Andrea; Ehrig, Hartmut; Montanari, Ugo; Ribeiro, Leila; Rozenberg, Grzegorz, Third International Conference on Graph Transformations, Lecture Notes in Computer Science, vol. 4178, (2006), Springer-Verlag), 445-460 · Zbl 1156.68347
[44] Hermann, Frank; Kastenberg, Harmen; Modica, Tony, Towards translating graph transformation approaches by model transformations, Electron. Commun. EASST, 4, (2006)
[45] Hermann, Frank; Corradini, Andrea; Ehrig, Hartmut, Analysis of permutation equivalence in \(\mathcal{M}\)-adhesive transformation systems with negative application conditions, Math. Structures Comput. Sci., 24, 4, (2014) · Zbl 1342.68179
[46] Hristakiev, Ivaylo; Plump, Detlef, A unification algorithm for GP 2, Electron. Commun. EASST, 71, (2014)
[47] Carlos Lemor, Luiz; da Costa Cavalheiro, Simone André; Foss, Luciana, Proof tactics for theorem proving graph grammars through rodin, Rev. Inf. Teór. Apl., 22, 1, 190-241, (2015)
[48] Carlos Lemos, Luiz; da Costa Cavalheiro, Simone André; Foss, Luciana, Theorem proving graph grammars: strategies for discharging proof obligations, (Iyoda, Juliano; de Moura, Leonardo Mendonça, 16th Brazilian Symposium on Formal Methods: Foundations and Applications, Lecture Notes in Computer Science, vol. 8195, (2013), Springer-Verlag), 147-162 · Zbl 1409.68173
[49] Kastenberg, Harmen, Towards attributed graphs in groove: work in progress, Electron. Notes Theor. Comput. Sci., 154, 2, 47-54, (2006) · Zbl 1273.68192
[50] König, Barbara; Kozioura, Vitali, Towards the verification of attributed graph transformation systems, (4th International Conference on Graph Transformations, Lecture Notes in Computer Science, vol. 5214, (2008), Springer-Verlag), 305-320 · Zbl 1175.68226
[51] Korff, Martin, Generalized graph structures with application to concurrent object-oriented systems, (1995), TU Berlin, Ph.D. thesis
[52] Kwiatkowska, Marta; Norman, Gethin; Parker, David, Prism 4.0: verification of probabilistic real-time systems, (23rd International Conference on Computer Aided Verification, CAV’11, (2011), Springer-Verlag), 585-591
[53] Löwe, Michael, Algebraic approach to single-pushout graph transformation, Theoret. Comput. Sci., 109, 1-2, 181-224, (1993) · Zbl 0787.18001
[54] Löwe, Michael; Korff, Martin; Wagner, Annika, An algebraic framework for the transformation of attributed graphs, (Term Graph Rewriting: Theory and Practice, (1993), John Wiley and Sons Ltda.), 185-199
[55] Manna, Zohar; Pnueli, Amir, The temporal logic of reactive and concurrent systems - specification, (1992), Springer-Verlag · Zbl 0753.68003
[56] Manning, Greg; Plump, Detlef, The GP programming system, Electron. Commun. EASST, 10, (2008) · Zbl 1283.68116
[57] Nipkow, Tobias; Paulson, Lawrence C.; Wenzel, Markus, Isabelle/HOL: A proof assistant for higher-order logic, Lecture Notes in Computer Science, vol. 2283, (2002), Springer-Verlag · Zbl 0994.68131
[58] Oliveira, Marcel; Cavalcanti, Ana; Woodcock, Jim, Unifying theories in proofpower-Z, (Dunne, Steve; Stoddart, Bill, First International Symposium on Unifying Theories of Programming, Lecture Notes in Computer Science, vol. 4010, (2006), Springer-Verlag), 123-140 · Zbl 1186.68090
[59] Orejas, Fernando, Symbolic graphs for attributed graph constraints, J. Symbolic Comput., 46, 3, 294-315, (2011) · Zbl 1298.68121
[60] Orejas, Fernando; Lambers, Leen, Symbolic attributed graphs for attributed graph transformation, Electron. Commun. EASST, 30, (2010) · Zbl 1306.68084
[61] Pennemann, Karl-Heinz, An algorithm for approximating the satisfiability problem of high-level conditions, Electron. Notes Theor. Comput. Sci., 213, 1, 75-94, (2008) · Zbl 1283.68211
[62] Pennemann, Karl-Heinz, Resolution-like theorem proving for high-level conditions, (Ehrig, Hartmut; Heckel, Reiko; Rozenberg, Grzegorz; Taentzer, Gabriele, International Conference on Graph Transformations, Lecture Notes in Computer Science, vol. 5214, (2008), Springer-Verlag), 289-304 · Zbl 1175.03008
[63] Percebois, Christian; Martin, Strecker; Tran, Hanh Nhi, Rule-level verification of graph transformations for invariants based on edges’ transitive closure, (Hierons, Robert M.; Merayo, Mercedes G.; Bravetti, Mario, 11th International Conference on Software Engineering and Formal Methods, Lecture Notes in Computer Science, vol. 8137, (2013), Springer-Verlag), 106-121
[64] Peuser, Christoph; Habel, Annegret, Attribution of graphs by composition of \(m, n\)-adhesive categories, (6th International Workshop on Graph Computation Models, vol. 1403, (2015)), 66-81, CEUR-WS.org
[65] Plump, Detlef; Escobar, Santiago, The design of GP 2, 10th International Workshop on Reduction Strategies in Rewriting and Programming, EPTCS, 82, 1-16, (2011)
[66] Plump, Detlef; Bak, Christopher, Rooted graph programs, Electron. Commun. EASST, 54, (2012)
[67] Poskitt, Christopher M.; Plump, Detlef, Hoare-style verification of graph programs, Fund. Inform., 118, 1-2, 135-175, (2012) · Zbl 1284.68333
[68] Poskitt, Christopher M.; Plump, Detlef, Verifying total correctness of graph programs, Revised Selected Papers, Graph Computation Models, Electron. Commun. EASST, 61, (2013) · Zbl 1425.68080
[69] Rensink, Arend, The GROOVE simulator: a tool for state space generation, (Pfalz, J.; Nagl, M.; Böhlen, B., Applications of Graph Transformations with Industrial Relevance, Lecture Notes in Computer Science, vol. 3062, (2004), Springer-Verlag), 479-485
[70] Ribeiro, Leila; Dotti, Fernando Luís; da Costa, Simone André; Dillenburg, Fabiane Cristine, Towards theorem proving graph grammars using event-B, Electron. Commun. EASST, 30, (2010)
[71] (Rozenberg, Grzegorz, Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1: Foundation, (1997), World Scientific)
[72] Strecker, Martin, Modeling and verifying graph transformations in proof assistants, Electron. Notes Theor. Comput. Sci., 203, 1, 135-148, (2008) · Zbl 1279.68297
[73] Strecker, Martin, Locality in reasoning about graph transformations, (4th International Conference on Applications of Graph Transformations with Industrial Relevance, AGTIVE’11, (2012), Springer-Verlag), 169-181
[74] Strecker, Martin, Interactive and automated proofs for graph transformations, Math. Structures Comput. Sci., (2014), 31 pages · Zbl 1398.68286
[75] Tanenbaum, Andrew S.; Wetherall, David J., Computer networks, (2011), Prentice Hall
[76] Tran, Hanh Nhi; Percebois, Christian, Towards a rule-level verification framework for property-preserving graph transformations, (Antoniol, Giuliano; Bertolino, Antonia; Labiche, Yvan, Fifth International IEEE Conference on Software Testing, Verification and Validation, (2012), IEEE Computer Society)
[77] Väänänen, Jouko, Second order logic, set theory and foundations of mathematics, (Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, (2012), Springer-Verlag), 371-380 · Zbl 1314.03014
[78] Varró, Dániel; Varró, Gergely; Pataricza, András, Designing the automatic transformation of visual languages, Sci. Comput. Program., 44, 2, 205-227, (2002) · Zbl 1014.68039
[79] Warmer, Jos; Kleppe, Anneke, The object constraint language: precise modeling with UML, (1999), Addison-Wesley Longman Publishing Co., Inc. · Zbl 1042.68757
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.