Formale Sprachen

Entwicklung korrekter Graphtransformationssysteme

Projektdauer: 2006-2008

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.

  • A. Habel und K. Pennemann, "Correctness of high-level transformation systems relative to nested conditions," Mathematical Structures in Computer Science, vol. 19, pp. 1-52, 2009.
    @article{Habel-Pennemann09a,
      author = {Habel, Annegret and Pennemann, Karl-Heinz},
      title = {Correctness of high-level transformation systems relative to nested conditions},
      journal = {Mathematical Structures in Computer Science},
      volume = {19},
      pages = {1-52},
      year = {2009},
      publists = {dcgts,selected,topics},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/mscs-HP09.pdf},
      url = {http://journals.cambridge.org/action/displayFulltext?type=1&fid=5376264&jid=MSC&volumeId=19&issueId=02&aid=5376256} }
  • C. Bley, "Ein Editor zum Erstellen von Graphprogrammen," 2008.
    @techreport{Bley08a,
      author = {Christian Bley},
      title = {{Ein Editor zum Erstellen von Graphprogrammen}},
      year = {2008},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/report_graphprograms.pdf} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    K. Azab, "Editing Nested Constraints and Application Conditions," in Proc. Proc. Int. Workshop on Graph Computation Models (GCM'08), 2008, pp. 35-42.
    @inproceedings{Azab08a,
      author = {Azab, Karl},
      title = {Editing Nested Constraints and Application Conditions},
      booktitle = {Proc. Int. Workshop on Graph Computation Models (GCM'08)},
      editor = {Habel, A. and Mosbah, M.},
      year = {2008},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/editing_gcm.pdf},
      pages = {35-42},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/editing_long.pdf} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    K. Azab und A. Habel, "High-level programs and program conditions," in Proc. Graph Transformations (ICGT'08), 2008, pp. 211-225.
    @inproceedings{Azab-Habel08a,
      author = {Azab, Karl and Habel, Annegret},
      title = {High-level programs and program conditions},
      booktitle = {Graph Transformations (ICGT'08)},
      year = {2008},
      series = {Lecture Notes in Computer Science},
      volume = {5214},
      pages = {211-225},
      publisher = {Springer-Verlag},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/program-conditions.pdf},
      url = {http://springerlink.metapress.com/content/v0w814m5125603h2/} }
  • [proceedings] bibtex | Dokument aufrufen Dokument aufrufen
    Proc. Second Int. Workshop on Graph Computation Models (GCM 2008), 52 pages, Leichester, United Kingdom, September, 2008.
    @proceedings{Habel-Mosbah08a, editor = {Habel, Annegret and Mosbah, Mohamed},
      title = {Proc. Second Int. Workshop on Graph Computation Models (GCM 2008), 52 pages, Leichester, United Kingdom, September},
      publisher = {},
      year = {2008},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/gcm-proceedings-v.1.0.pdf} }
  • M. Mosbah und A. Habel, Workshop on Graph Computation ModelsSpringer, 2008.
    @misc{Mosbah-Habel08a,
      author = {Mosbah, Mohamed and Habel, Annegret},
      title = {Workshop on Graph Computation Models},
      booktitle = {Graph Transformations (ICGT 2008)},
      publisher = {Springer},
      series = {Lecture Notes in Computer Science},
      volume = {5214},
      pages = {460-462},
      year = {2008},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/gcm2008.pdf},
      url = {http://springerlink.metapress.com/content/u16670u615359414/} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    K. Pennemann, "Resolution-like theorem proving for high-level conditions," in Proc. Graph Transformations (ICGT'08), 2008, pp. 289-304.
    @inproceedings{Pennemann08b,
      author = {Pennemann, Karl-Heinz},
      title = {Resolution-like theorem proving for high-level conditions},
      booktitle = {Graph Transformations (ICGT'08)},
      year = {2008},
      series = {Lecture Notes in Computer Science},
      volume = {5214},
      pages = {289-304},
      publisher = {Springer-Verlag},
      publists = {dcgts,selected},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/procon.pdf},
      url = {http://springerlink.metapress.com/content/p01554m107170572/} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    K. Pennemann, "Development of correct graph transformation systems -- Preliminary abstract," in Proc. Graph Transformations (ICGT'08 Doctoral Symposium), 2008, pp. 508-510.
    @inproceedings{Pennemann08c,
      author = {Pennemann, Karl-Heinz},
      title = {Development of correct graph transformation systems -- {P}reliminary abstract},
      booktitle = {Graph Transformations (ICGT'08 Doctoral Symposium)},
      year = {2008},
      series = {Lecture Notes in Computer Science},
      volume = {5214},
      pages = {508-510},
      publisher = {Springer-Verlag},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/icgt2008ds.pdf},
      url = {http://springerlink.metapress.com/content/1p077n327p212262/} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    K. Azab und K. Pennemann, "Type Checking C++ Template Instantiation by Graph Programs," in Proc. Proc. Int. Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'08), 2008, pp. 249-262.
    @inproceedings{Azab-Pennemann08a,
      author = {Azab, Karl and Pennemann, Karl-Heinz},
      title = {Type Checking {C}++ Template Instantiation by Graph Programs},
      booktitle = {Proc. Int. Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'08)},
      volume = {10},
      pages = {249-262},
      year = {2008},
      publisher = {Electronic Communications of the EASST},
      issn = {1863-2122},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/templates.pdf},
      url = {http://journal.ub.tu-berlin.de/index.php/eceasst/issue/view/19} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    K. Pennemann, "An Algorithm for Approximating the Satisfiability Problem of High-level Conditions," in Proc. Proc. Graph Transformation for Verification and Concurrency (GT-VC'07), 2008, pp. 75-94.
    @inproceedings{Pennemann07a,
      author = {Pennemann, Karl-Heinz},
      title = {An Algorithm for Approximating the Satisfiability Problem of High-level Conditions},
      booktitle = {Proc. Graph Transformation for Verification and Concurrency (GT-VC'07)},
      year = {2008},
      series = {Electronic Notes in Theoretical Computer Science},
      volume = {213},
      issue = {1},
      pages = {75-94},
      publisher = {Elsevier},
      publists = {dcgts,selected},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/seeksat.pdf} }
  • K. Azab und K. Pennemann, "Type Checking C++ Template Instantiation by Graph Programs," Universität Oldenburg, Berichte aus dem Department für Informatik 04/07, 24 pages, 2007.
    @techreport{Azab-Pennemann07a,
      author = {Azab, Karl and Pennemann, Karl-Heinz},
      title = {Type Checking {C}++ Template Instantiation by Graph Programs},
      type = {{Berichte aus dem Department f\"ur Informatik}},
      number = {04/07, 24 pages},
      institution = {Universit\"at Oldenburg},
      year = {2007},
      issn = {0946-2910},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/templates_long.pdf} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    K. Azab, A. Habel, K. Pennemann, und C. Zuckschwerdt, "ENFORCe: A System for Ensuring Formal Correctness of High-level Programs," in Proc. Proc. 3rd International Workshop on Graph Based Tools (GraBaTs'06), 2007, pp. 82-93.
    @inproceedings{Azab-Habel-Pennemann-Zuckschwerdt06a,
      author = {Azab, Karl and Habel, Annegret and Pennemann, Karl-Heinz and Zuckschwerdt, Christian},
      title = {{ENFORCe}: A System for Ensuring Formal Correctness of High-level Programs},
      booktitle = {Proc. 3rd International Workshop on Graph Based Tools (GraBaTs'06)},
      year = {2007},
      volume = {1},
      publisher = {Electronic Communications of the EASST},
      pages = {82-93},
      issn = {1863-2122},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/enforce.pdf},
      url = {http://journal.ub.tu-berlin.de/index.php/eceasst/issue/view/9} }
  • C. Zuckschwerdt, "Ein System zur Transformation von Konsistenz in Anwendungsbedingungen," Universität Oldenburg, Berichte aus dem Department für Informatik 11/06, 114 pages, 2006.
    @techreport{Zuckschwerdt06a,
      author = {Zuckschwerdt, Christian},
      title = {{Ein System zur Transformation von Konsistenz in Anwendungsbedingungen}},
      type = {{Berichte aus dem Department f\"ur Informatik}},
      number = {11/06, 114 pages},
      institution = {Universit\"at Oldenburg},
      year = {2006},
      issn = {0946-2910},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/coconut-techreport.pdf} }
  • H. Ehrig, A. Habel, J. Padberg, und U. Prange, "Adhesive High-Level Replacement Systems: A New Categorical Framework for Graph Transformation," Fundamenta Informaticae, vol. 74, pp. 1-29, 2006.
    @article{Ehrig-Habel-Padberg-Prange06a,
      author = {Ehrig, Hartmut and Habel, Annegret and Padberg, Julia and Prange, Ulrike},
      title = {Adhesive High-Level Replacement Systems: A New Categorical Framework for Graph Transformation},
      journal = {Fundamenta Informaticae},
      volume = {74},
      pages = {1-29},
      year = {2006},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/fundamenta-ahlr.pdf} }
  • A. Habel, K. Pennemann, und A. Rensink, "Weakest Preconditions for High-Level Programs (Long Version)," Universität Oldenburg, Berichte aus dem Department für Informatik 8/06, 35 pages, 2006.
    @techreport{Habel-Pennemann-Rensink06b,
      author = {Habel, Annegret and Pennemann, Karl-Heinz and Rensink, Arend},
      title = {Weakest Preconditions for High-Level Programs (Long Version)},
      type = {{Berichte aus dem Department f\"ur Informatik}},
      number = {8/06, 35 pages},
      institution = {Universit\"at Oldenburg},
      year = {2006},
      issn = {0946-2910},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/hpr06-long.pdf} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    A. Habel, K. Pennemann, und A. Rensink, "Weakest Preconditions for High-Level Programs," in Proc. Graph Transformations (ICGT'06), 2006, pp. 445-460.
    @inproceedings{Habel-Pennemann-Rensink06a,
      author = {Habel, Annegret and Pennemann, Karl-Heinz and Rensink, Arend},
      title = {Weakest Preconditions for High-Level Programs},
      booktitle = {Graph Transformations (ICGT'06)},
      year = {2006},
      series = {Lecture Notes in Computer Science},
      volume = {4178},
      pages = {445-460},
      publisher = {Springer-Verlag},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/weakestpreconditions.pdf},
      url = {http://springerlink.metapress.com/content/bj1683345uv61r68/} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    A. Habel und K. Pennemann, "Satisfiability of High-Level Conditions," in Proc. Graph Transformations (ICGT'06), 2006, pp. 430-444.
    @inproceedings{Habel-Pennemann06b,
      author = {Habel, Annegret and Pennemann, Karl-Heinz},
      title = {Satisfiability of High-Level Conditions},
      booktitle = {Graph Transformations (ICGT'06)},
      year = {2006},
      series = {Lecture Notes in Computer Science},
      volume = {4178},
      pages = {430-444},
      publisher = {Springer-Verlag},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/satisfiability.pdf},
      url = {http://www.springerlink.com/content/3h1012651r702875/} }
  • H. Ehrig, K. Ehrig, A. Habel, und K. Pennemann, "Theory of Constraints and Application Conditions: From Graphs to High-Level Structures," Fundamenta Informaticae, vol. 74, iss. 1, pp. 135-166, 2006.
    @article{Ehrig-Ehrig-Habel-Pennemann06a,
      author = {Ehrig, Hartmut and Ehrig, Karsten and Habel, Annegret and Pennemann, Karl-Heinz},
      title = {Theory of Constraints and Application Conditions: From Graphs to High-Level Structures},
      journal = {Fundamenta Informaticae},
      volume = {74},
      number = {1},
      pages = {135-166},
      year = {2006},
      publists = {dcgts,selected},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/fundamenta-constraints.ps.gz} }
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    A. Habel und K. Pennemann, "Nested Constraints and Application Conditions for High-Level Structures," in Proc. Formal Methods in Software and System Modeling, 2005, pp. 294-308.
    @inproceedings{Habel-Pennemann05a,
      author = {Habel, Annegret and Pennemann, Karl-Heinz},
      title = {Nested Constraints and Application Conditions for High-Level Structures},
      editor = {Kreowski, Hans-J\"org and Montanari, Ugo and Orejas, Fernando and Rozenberg, Grzegorz and Taentzer, Gabriele},
      booktitle = {Formal Methods in Software and System Modeling},
      publisher = {Springer-Verlag},
      series = {Lecture Notes in Computer Science},
      volume = {3393},
      pages = {294-308},
      year = {2005},
      publists = {dcgts},
      url = {http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/nested-constraints.ps.gz},
      url = {http://springerlink.metapress.com/content/j90uycf5wpey/#section=560146} }