Grafische Constraints zur Entwicklung korrekter Graphtransformationssysteme und zur Verifikation von Graphprogrammen
Final Report Abstract
Zur Modellierung von Systemen und Systemeigenschaften werden h¨aufig Graphtransformationssysteme und Graphbedingungen verwendet: Die Beschreibung von Systemzust¨anden erfolgt durch graphische Strukturen wie z.B. Petri-Netze, Graphen, Hypergraphen und attributierte Graphen, die Beschreibung von Zustands ¨anderungen erfolgt durch Strukturtransformationen wie z.B. Netz-, Graph- , Hypergraph- und attributierte Graph-Transformationen und die Beschreibung von Systemeigenschaften erfolgt textuell durch p¨adikatenlogische Formeln oder graphisch durch graphische Bedingungen, wie z.B. Netz-, Graph-, Hypergraph-, attributierte Graph-Bedingungen. Zur gemeinsamen Behandlung graph-¨ahnlicher Strukturen werden schwach adhesive HLR Kategorien, high-level Strukturen, Transformationssysteme und Bedingungen betrachtet alle Konstruktionen auf high-level Ebene durchgef¨uhrt; die Resultate lassen sich dann z.B. auf die Kategorien der Netze, Graphen, Hypergraphen und attributierte Graphen anwenden. Das neue Konzept der geschachtelten Bedingungen erm¨oglicht eine graphische Beschreibung von Systemeigenschaften. Es gibt es zwei naheliegende Erf¨ullbarkeits- Begriffe, A- und M-Erf¨ullbarkeit, wobei A die Klasse aller Morphismen undM eine Klasse von Monomorphismen bezeichnet. In schwach adhesive HLR-Kategorien, die strikt abgeschlossen ist unter Dekomposition sind, sind A- und M-Erf¨ullbarkeit von geschachtelten Bedingungen ausdrucks-¨aquivalent sind. Die Fallstudien zeigen, dass geschachtelte Bedingungen mit M-Erf¨ullbarkeit ein ad¨aquates Konzept f¨ur die Beschreibung von Systemeigenschaften ist. Geschachtelte Graphbedingungen und pr¨adikatenlogische Formeln erster Stufe auf Graphen sind ausdrucks-¨aquivalent. Als Konsequenz daraus ergibt sich die Unentscheidbarkeit des Implikationsproblems f¨ur geschachtelte Bedingungen. Die Transformation von geschachtelten Graphbedingungen in pr¨adikatenlogische Formeln erster Stufe kann genutzt werden, um geschachtelte Bedingungen als Eingabe f¨ur Theorembeweiser umzuwandeln und ein Semi-Entscheidungsverfahren f¨ur das Implikationsproblems zu erhalten. Eine Standardmethode zum Nachweis der Korrektheit ist die Konstruktion einer schw¨achsten Vorbedingung des Programms relativ zu der Nachbedingung und der Nachweis, dass die Vorbedingung die schw¨achste Vorbedingung impliziert. Diese Methode l¨asst sich auf high-level Programmemit high-level Vor- und Nachbedingung ¨ubertragen. Dar¨uber hinaus sind mehrere Semi-Entscheidungsverfahren f¨ur das Implikationsproblem von geschachtelten Bedingungen entwickelt worden. Zusammenfassend erh¨alt man damit eine Semi-Entscheidungsverfahren f¨ur die Korrektheit von Programmen. Das System ENFORCe zur Sicherstellung formaler Korrektheit von high-level Programmen stellt verschiedenen Methoden zur Untersuchung auf Korrektheit und zur Transformation in eine korrektes Programm zur Verf¨ugung. Um eine allgemein verwendbare Implementierung f¨ur die Konstruktion schw¨achster Vorbedingungen von Programmen zu erhalten werden die Konstruktionen auf high-level Ebene von den strukturspezifischen Konstruktionen getrennt. Es besitzt Editoren zum Erstellen von Graphprogramme und Graphbedingungen.
Publications
- [16] C. Zuckschwerdt. Ein System zur Transformation von Konsistenz- in Anwendungsbedingungen. Technischer Bericht 11/06, Universit¨at Oldenburg, 114 Seiten, 2006.
- A. Habel, K.-H. Pennemann, A. Rensink. Weakest preconditions for highlevel programs. In Graph Transformations (ICGT 2006), Lecture Notes in Computer Science 4178, 445¿460, 2006. Langfassung: Technischer Bericht 8/06, Universit¨at Oldenburg, 35 Seiten, 2006.
- A. Habel, K.-H. Pennemann. Satisfiability of high-level conditions. In Graph Transformations (ICGT 2006), Lecture Notes in Computer Science 4178, 430¿444, 2006.
- H. Ehrig, A. Habel, J. Padberg, U. Prange. Adhesive high-level replacement systems: A new categorical framework for graph transformation. Fundamenta Informaticae, 74(1): 1¿29, 2006.
- H. Ehrig, K. Ehrig, A. Habel, K.-H. Pennemann. Theory of constraints and application conditions: From graphs to high-level structures. Fundamenta Informaticae, 74(1):135¿166, 2006.
- K. Azab, A. Habel, K.-H. Pennemann, C. Zuckschwerdt. ENFORCe: A system for ensuring formal correctness of high-level programs. In Proc. of the Third International .Workshop on Graph Based Tools (GraBaTs¿06), Electronic Communications of the EASST, Vol. 1, 82-93, 2007
- K. Azab, A. Habel. High-level programs and program conditions. In Graph Transformations (ICGT 2008), Lecture Notes in Computer Science 5214, 211¿225, 2008.
- K. Azab, K.-H. Pennemann. Type checking C++ template instantiation by graph programs. In Proc. International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT¿08), Electronic Communications of the EASST, 249¿262, 2008. Langfassung: Technischer Bericht 4/07, Universit¨at Oldenburg, 24 Seiten, 2007.
- K. Azab. Editing nested graph conditions and application conditions. In A. Habel, M. Mosbah, editors, Proc. 2nd International Workshop on Graph Computation Models (GCM 2008), Leicester, United Kingdom, 35¿ 42, 2008.
- K.-H. Pennemann. An algorithm for approximating the satisfiability problem of high-level conditions. In Proc. International . Workshop on Graph Transformation for Verification and Concurrency (GT-VC¿07), Electronic Notes in Theoretical Computer Science 213, 75¿94, 2008. (Siehe online unter: http://formale-sprachen.informatik.uni-oldenburg.de/pub/index.html)
- K.-H. Pennemann. Development of correct graph transformation systems. In Graph Transformations (ICGT 2008), Doctoral Symposium, Lecture Notes in Computer Science 5214, 508¿510, 2008.
- K.-H. Pennemann. Resolution-like theorem proving for high-level conditions. In Graph Transformations (ICGT 2008), Lecture Notes in Computer Science 5214, 289¿304, 2008.
