Graphs, Recognizability and Verification (GaReV)

• Applicant: Professorin Dr. Barbara König
• Subject Area: Theoretical Computer Science
• Term: from 2010 to 2016
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 173310673

• Final Report Year: 2016

Final Report Abstract

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.

Publications

• A general framework for well-structured graph transformation systems. Information and Computation
  Barbara König and Jan Stückrath
  (See online at https://doi.org/10.1016/j.ic.2016.03.005)
• 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
  (See online at https://doi.org/10.1007/978-3-662-44584-6_32)
• 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
  (See online at https://doi.org/10.1007/978-3-319-11439-2_6)
• 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
  (See online at https://doi.org/10.1007/978-3-662-44602-7_15)
• 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
  (See online at https://doi.org/10.1007/978-3-319-08918-8_33)
• 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
  (See online at https://doi.org/10.1007/978-3-319-21145-9_4)
• 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
  (See online at https://doi.org/10.1016/j.scico.2014.08.006)
• Verification of Evolving Graph Structures (Dagstuhl Seminar 15451). Dagstuhl Reports, 5(11), 2015
  Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, and Viktor Vafeiadis
  (See online at https://dx.doi.org/10.4230/DagRep.5.11.1)
• Verification of Well-Structured Graph Transformation Systems. PhD thesis, Universität Duisburg-Essen, 2016
  Jan Stückrath