Entwicklung korrekter Graphtransformationssysteme

 

1 Entwicklung korrekter Graphtransformationssysteme

Projektdauer: 2 Jahre

Finanzierung durch: Deutsche Forschungsgemeinschaft (DFG)

Zusammenfassung des Forschungsvorhabens:

Für die Entwicklung korrekter Graphtransformationssysteme und Graphprogramme sollen theoretische Grundlagen und daraus resultierende Konzepte entwickelt werden. Als Sprache zur Spezifikation von Programmeigenschaften sollen (an Stelle von Formeln der Prädikatenlogik) grafische Constraints untersucht und verwendet werden, die sowohl geeignet erscheinen, Anforderungen an ein System zu beschreiben als auch Schlüsse über das Systemverhalten zu ziehen. Weiterhin sollen Constraint-Transformationen über Regeln, Mengen von Regeln, sequentielle Komposition von Regeln und iterierte Graphprogramme untersucht werden und Entscheidungs- beziehungsweise Semi-Entscheidungsverfahren für das Implikationsproblem von grafischen Constraints entwickelt werden. Die Anwendbarkeit der Konzepte soll durch geeignete Fallstudien nachgewiesen werden. Begleitend sollen Implementierungen erfolgen, mit der Absicht, die wesentlichen Schritte zu automatisieren, um schließlich ein Werkzeug zu erhalten, dass die Synthese von korrekten Graphtransformationssystemen und die Verifikation von Graphprogrammen unterstützt.

 

2 Veröffentlichungen

2.1 Zeitschriftenveröffentlichungen

[HP09]

Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science, 19:1-52, 2009.
[ .pdf ]

[EHPP06]

Hartmut Ehrig, Annegret Habel, Julia Padberg, and Ulrike Prange. Adhesive high-level replacement systems: A new categorical framework for graph transformation. Fundamenta Informaticae, 74:1-29, 2006.
[ .pdf ]

[EEHP06]

Hartmut Ehrig, Karsten Ehrig, Annegret Habel, and Karl-Heinz Pennemann. Theory of constraints and application conditions: From graphs to high-level structures. Fundamenta Informaticae, 74:135-166, 2006.
[ .ps.gz ]

2.2 Konferenz- und Sammelbeiträge

[Aza08]

Karl Azab. Editing nested constraints and application conditions. In A. Habel and M. Mosbah, editors, Proc. Int. Workshop on Graph Computation Models (GCM'08), pages 35-42, 2008. Download Long version.
[ .pdf ]

[Pen08c]

Karl-Heinz Pennemann. Resolution-like theorem proving for high-level conditions. In Graph Transformations (ICGT'08), volume 5214 of Lecture Notes in Computer Science, pages 289-304. Springer-Verlag, 2008.
[ .pdf ]

[Pen08b]

Karl-Heinz Pennemann. Development of correct graph transformation systems - Preliminary abstract. In Graph Transformations (ICGT'08 Doctoral Symposium), volume 5214 of Lecture Notes in Computer Science, pages 508-510. Springer-Verlag, 2008.
[ .pdf ]

[AH08]

Karl Azab and Annegret Habel. High-level programs and program conditions. In Graph Transformations (ICGT'08), volume 5214 of Lecture Notes in Computer Science, pages 211-225. Springer-Verlag, 2008.
[ .pdf ]

[AP08]

Karl Azab and Karl-Heinz Pennemann. Type checking C++ template instantiation by graph programs. In Proc. Int. Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'08), pages 249-262. Electronic Communications of EASST, 2008.
[ .pdf ]

[Pen08a]

Karl-Heinz Pennemann. An algorithm for approximating the satisfiability problem of high-level conditions. In Proc. Graph Transformation for Verification and Concurrency (GT-VC'07), volume 213 of Electronic Notes in Theoretical Computer Science, pages 75-94. Elsevier, 2008.
[ .pdf ]

[AHPZ07]

Karl Azab, Annegret Habel, Karl-Heinz Pennemann, and Christian Zuckschwerdt. ENFORCe: A system for ensuring formal correctness of high-level programs. In Proc. 3rd International Workshop on Graph Based Tools (GraBaTs'06), volume 1, pages 82-93. Electronic Communications of EASST, 2007.
[ .pdf ]

[HPR06]

Annegret Habel, Karl-Heinz Pennemann, and Arend Rensink. Weakest preconditions for high-level programs. In Graph Transformations (ICGT'06), volume 4178 of Lecture Notes in Computer Science, pages 445-460. Springer-Verlag, 2006.
[ .pdf ]

[HP06]

Annegret Habel and Karl-Heinz Pennemann. Satisfiability of high-level conditions. In Graph Transformations (ICGT'06), volume 4178 of Lecture Notes in Computer Science, pages 430-444. Springer-Verlag, 2006.
[ .pdf ]

[HP05]

Annegret Habel and Karl-Heinz Pennemann. Nested constraints and application conditions for high-level structures. In Hans-Jörg Kreowski, Ugo Montanari, Fernando Orejas, Grzegorz Rozenberg, and Gabriele Taentzer, editors, Formal Methods in Software and System Modeling, volume 3393 of Lecture Notes in Computer Science, pages 294-308. Springer-Verlag, 2005.
[ .ps.gz ]

2.3 Weitere Publikationen

[Ble08]

Christian Bley. Ein Editor zum Erstellen von Graphprogrammen. Technical report, 2008.
[ .pdf ]

[MH08]

Mohamed Mosbah and Annegret Habel. Workshop on graph computation models, 2008.
[ .pdf ]

[AP07]

Karl Azab and Karl-Heinz Pennemann. Type checking C++ template instantiation by graph programs. Berichte aus dem Department für Informatik 04/07, 24 pages, Universität Oldenburg, 2007.
[ .pdf ]

[Zuc06]

Christian Zuckschwerdt. Ein System zur Transformation von Konsistenz in Anwendungsbedingungen. Berichte aus dem Department für Informatik 11/06, 114 pages, Universität Oldenburg, 2006.
[ .pdf ]

[HPR06]

Annegret Habel, Karl-Heinz Pennemann, and Arend Rensink. Weakest preconditions for high-level programs (long version). Berichte aus dem Department für Informatik 8/06, 35 pages, Universität Oldenburg, 2006.
[ .pdf ]