Graphen, Erkennbarkeit und Verifikation (GaReV)

• Antragstellerin: Professorin Dr. Barbara König
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2010 bis 2016
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 173310673

• Erstellungsjahr: 2016

Zusammenfassung der Projektergebnisse

Ein Teilgebiet der Informatik ist die Verifikation von Software-Systemen. Dabei geht es darum, zu überprüfen, ob ein System die geforderten Eigenschaften hat, beispielsweise möchte man automatisch verifizieren, dass es zu keinem Laufzeitfehler kommt oder dass irgendwann ein korrektes Ergebnis erzeugt und ausgegeben wird. In diesem Gebiet werden Techniken entwickelt, die in der Praxis sehr nützlich sind, oft auf der Grundlage von mathematisch tiefgehenden und komplexen Resultaten. Eine besonders große Herausforderung ist die Verifikation von verteilten Systemen, bei denen viele Komponenten unabhängig voneinander agieren. Der Ansatz in dem Projekt GaRev ist, solche Systeme mit Hilfe von Graphen, d.h. durch Netze, bestehend aus Knoten und Kanten, zu modellieren. Die Dynamik solcher Systeme wird mit Hilfe einer Menge von Regeln spezifiziert. Dabei wurden Methoden aus der Theorie der erkennbaren Graphsprachen, der Graphentheorie und der Verifikation von wohl-strukturierten Transitionssystemen geeignet angepasst, implementiert und evaluiert. Neben theoretischen und grundlagenorientierten Ergebnissen entstanden auch drei prototypische Software-Werkzeuge: RAVEN – eine Tool-Suite für Graph-Automaten; UNCOVER – ein Werkzeug für die Erreichbarkeits- und Überdeckbarkeitsanalyse, basierend auf wohl-strukturierten Transitionssystemen; GREZ – ein Terminierungswerkzeug für Graphtransformationssysteme. Die Evaluierung der entsprechenden Methoden zeigte teilweise sehr gute und vielversprechende Laufzeitergebnisse. Bei RAVEN wurden die Laufzeiten durch den Einsatz symbolischer Techniken deutlich verbessert. Die Werkzeuge wurden in zahlreichen Fallstudien getestet, insbesonderen wurden mit UNCOVER verschiedene Protokolle für verteilte Systeme analysiert. Das Projekt trug mit dazu bei, den Stand auf dem Gebiet der Verifikation dynamischer Systeme zu verbessern.

Projektbezogene Publikationen (Auswahl)

• A general framework for well-structured graph transformation systems. Information and Computation
  Barbara König and Jan Stückrath
  
• A general framework for well-structured graph transformation systems. In Proc. of CONCUR ’14, pages 467–481. Springer, 2014. LNCS/ARCoSS 8704
  Barbara König and Jan Stückrath
  
• Graph Automata and Their Application to the Verification of Dynamic Systems. PhD thesis, Universität Duisburg-Essen, March 2014
  Christoph Blume
  
• Parameterized verification of graph transformation systems with whole neighbourhood operations. In Proc. of RP ’14 (Reachability Problems), volume 8762 of LNCS, pages 72–84. Springer, 2014
  Giorgio Delzanno and Jan Stückrath
  
• Termination analysis for graph transformation systems. In Proc. of TCS ’14, IFIP AICT, pages 179–194. Springer, 2014. LNCS 8705
  H.J. Sander Bruggink, Barbara König, and Hans Zantema
  
• Termination of cycle rewriting. In Proc. of RTA-TLCA ’14, pages 476–490. Springer, 2014. LNCS 8560
  Hans Zantema, H.J. Sander Bruggink, and Barbara König
  
• Proving termination of graph transformation systems using weighted type graphs over semirings. In Proc. of ICGT ’15 (International Conference on Graph Transformation). Springer, 2015. LNCS 9151
  H.J. Sander Bruggink, Barbara König, Dennis Nolte, and Hans Zantema
  
• Robustness and closure properties of recognizable languages in adhesive categories. Science of Computer Programming, 104:71–98, 2015
  H.J. Sander Bruggink, Barbara König, and Sebastian Küpper
  
• Verification of Evolving Graph Structures (Dagstuhl Seminar 15451). Dagstuhl Reports, 5(11), 2015
  Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, and Viktor Vafeiadis
  
• Verification of Well-Structured Graph Transformation Systems. PhD thesis, Universität Duisburg-Essen, 2016
  Jan Stückrath