Korrekte Modelltransformationen III (KorMoran III)

• Antragstellerinnen / Antragsteller: Professor Dr. Holger Giese; Professorin Dr. Sabine Glesner
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2009 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 148420506

• Erstellungsjahr: 2025

Zusammenfassung der Projektergebnisse

Eingebettete Systeme sind heutzutage allgegenwärtig. Durch immer größer werdende Rechenleistungen und Vernetzung solcher Systeme sind diese in der Lage, immer komplexere Aufgaben zu erfüllen. Diese Komplexität muss durch Softwaredesign beherrscht werden wofür standardisierte, bewährte Methoden der Softwaretechnik anzuwenden sind. Dazu zählt die modellgetriebene Entwicklung (MDE), die den Entwickler beim Design der abstrakten Anwendungsfälle bis zum konkreten, ausführbaren Code begleitet. Da auch die hierbei verwendeten Modelle sehr komplex sein können, wird Unterstützung benötigt um sicherzustellen, dass Modelltransformationen (bspw. Refactoring, Modellsynchronisation, Verfeinerung, Abstraktion) das Verhalten äquivalent bewahren und so sicherstellen, dass die abstrakten ursprünglichen Modelle den konkreten resultierenden Modellen (in Bezug auf Eigenschaften die in beiden Modellen erfasst werden) semantisch gleichen. In besonders sicherheitskritischen Bereichen gelten spezielle Qualitätsanforderungen an die Vertrauenswürdigkeit, die eine formale Verifikation von Spezifikationstreue und Verhaltensäquivalenzen notwendig machen. Das Projekt zielte darauf ab, automatisierte Methoden für die formale Verifikation von Modelltransformationen in Bezug auf Verhaltensäquivalenz zu entwickeln und zu evaluieren. Für die formale Erfassung von Modellen und Modelltransformationsprogrammen haben wir dabei als Ausgangspunkt Graphtransformationssysteme betrachtet. Im Rahmen des Projekts haben wir in mehreren Ausbaustufen, die sich aus verschiedenen Klassen von Analyseproblemen (Ergebnis- versus Transformationskorrektheit), Modellen (verschiedene Verhaltensmodelle) und Modelltransformationsprogrammen (Operational versus Relational) ergeben, feingliedrig Korrektheitsanalyseverfahren für Einzelmodelle, Modellpaare und letztlich Modelltransformationen erarbeitet wobei Verhaltensäquivalenz bzw. Verhaltensverfeinerung im Fokus stand. Werkzeuge wurden entwickelt und erweitert sowie anhand von Fallstudien evaluiert. Als besondere Anwendung standen Matlab/Simulink/Stateflow-Modelle im Zentrum der Betrachtung, da derartige Modelle in vielen sicherheitskritischen Anwendungen wie zum Bespiel der Automobilindustrie oder im Avionicsbereich eine wichtige Rolle spielen.

Projektbezogene Publikationen (Auswahl)

• Toward Bridging the Gap between Formal Semantics and Implementation of Triple Graph Grammars. 2010 Workshop on Model-Driven Engineering, Verification, and Validation, 19-24. IEEE.
  Giese, Holger; Hildebrandt, Stephan & Lambers, Leen
  
• Toward Bridging the Gap Between Formal Semantics and Implementation of Triple Graph Grammars. Tech. rep. 37. HPI, University of Potsdam, 2010.
  Holger Giese, Stephan Hildebrandt & Leen Lambers
  
• Iterative Development of Consistency-Preserving Rule-Based Refactorings. Lecture Notes in Computer Science, 123-137. Springer Berlin Heidelberg.
  Becker, Basil; Lambers, Leen; Dyck, Johannes; Birth, Stefanie & Giese, Holger
  
• Automatic Conformance Testing of Optimized Triple Graph Grammar Implementations. Lecture Notes in Computer Science, 238-253. Springer Berlin Heidelberg.
  Hildebrandt, Stephan; Lambers, Leen; Giese, Holger; Petrick, Dominic & Richter, Ingo
  
• Bridging the gap between formal semantics and implementation of triple graph grammars. Software & Systems Modeling, 13(1), 273-299.
  Giese, Holger; Hildebrandt, Stephan & Lambers, Leen
  
• Industrial case study on the integration of SysML and AUTOSAR with triple graph grammars. Tech. rep. 57. HPI, University of Potsdam, 2012.
  Holger Giese, Stephan Hildebrandt, Stefan Neumann & Sebastian Wätzoldt
  
• The MDELab tool framework for the development of correct model transformations with triple graph grammars. Proceedings of the First Workshop on the Analysis of Model Transformations, 33-34. ACM.
  Hildebrandt, Stephan; Lambers, Leen & Giese, Holger
  
• Toward Bridging the Gap between Formal Foundations and Current Practice for Triple Graph Grammars. Lecture Notes in Computer Science, 141-155. Springer Berlin Heidelberg.
  Golas, Ulrike; Lambers, Leen; Ehrig, Hartmut & Giese, Holger
  
• Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking. Lecture Notes in Computer Science, 249-263. Springer Berlin Heidelberg.
  Giese, Holger & Lambers, Leen
  
• “Attribute Handling for Bidirectional Model Transformations: The Triple Graph Grammar Case”. In: Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 49 (2012).
  Leen Lambers, Stephan Hildebrandt, Holger Giese & Fernando Orejas
  
• “Integration of Triple Graph Grammars and Constraints”. In: Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 54 (2012).
  Stephan Hildebrandt, Leen Lambers, Basil Becker & Holger Giese
  
• Complete Specification Coverage in Automatically Generated Conformance Test Cases for TGG Implementations. Lecture Notes in Computer Science, 174-188. Springer Berlin Heidelberg.
  Hildebrandt, Stephan; Lambers, Leen & Giese, Holger
  
• “Towards the Automatic Verification of Behavior Preservation at the Transformation Level for Operational Model Transformations”. In: Proceedings of the 4th Workshop on the Analysis of Model Transformations co-located with the 18th International Conference on Model Driven Engineering Languages and Systems (MODELS 2015), Ottawa, Canada, September 28, 2015. Ed. by Jürgen Dingel, Sahar Kokaly, Levi Lucio, Rick Salay, and Hans Vangheluwe. Vol. 1500. CEUR Workshop Proceedings. CEUR-WS.org, 2015, pp. 36–45.
  Johannes Dyck, Holger Giese, Leen Lambers, Sebastian Schlesinger & Sabine Glesner
  
• “Towards the verification of refactorings of hybrid simulink models”. In: Proceedings of the Third International Workshop on Verification and Program Transformation (VPT). Ed. by Andrei Nemytyk Alexei Lisitsa and Alberto Pettorossi. volume 199 of EPTCS, 2015.
  Sebastian Schlesinger, Paula Herber, Thomas Göthel & Sabine Glesner
  
• “Proving transformation correctness of refactorings for discrete and continuous simulink models”. In: ICONS 2016, The Eleventh International Conference on Systems, EMBEDDED 2016, International Symposium on Advances in Embedded Systems and Applications. 2016.
  Sebastian Schlesinger, Paula Herber, Thomas Göthel & Sabine Glesner
  
• Automatic Verification of Behavior Preservation at the Transformation Level for Relational Model Transformation. Tech. rep. 112. HPI, University of Potsdam, 2017.
  Johannes Dyck, Holger Giese & Leen Lambers
  
• Proving Correctness of Refactorings for Hybrid Simulink Models with Control Flow. Lecture Notes in Computer Science, 71-86. Springer International Publishing.
  Schlesinger, Sebastian; Herber, Paula; Göthel, Thomas & Glesner, Sabine
  
• Automatic verification of behavior preservation at the transformation level for relational model transformation. Software & Systems Modeling, 18(5), 2937-2972.
  Dyck, Johannes; Giese, Holger & Lambers, Leen
  
• Equivalence Checking for Hybrid Control Systems Modelled in Simulink. 2018 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C), 572-579. IEEE.
  Schlesinger, Sebastian; Herber, Paula; Gothel, Thomas & Glesner, Sabine
  
• Equivalence checking of Petri net models of programs using static and dynamic cut-points. Acta Informatica, 56(4), 321-383.
  Bandyopadhyay, Soumyadip; Sarkar, Dipankar & Mandal, Chittaranjan
  
• “Formal verification of model refactorings for hybrid control systems”. PhD thesis. Technical University of Berlin, Germany, 2018.
  Sebastian Schlesinger
  
• “Verified model refactorings for hybrid control systems”. In: PhD Forum Design Automation and Test in Europe (DATE) 2018. 2018.
  Sebastian Schlesinger, Paula Herber, Thomas Göthel & Sabine Glesner
  
• Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions. Lecture Notes in Computer Science, 257-275. Springer International Publishing.
  Schneider, Sven; Dyck, Johannes & Giese, Holger
  
• “Verification of graph transformation systems with k-inductive invariants”. PhD thesis. University of Potsdam, Germany, 2020.
  Johannes Dyck
  
• Translation validation of coloured Petri net models of programs on integers. Acta Informatica, 59(6), 725-759.
  Bandyopadhyay, Soumyadip; Sarkar, Dipankar; Mandal, Chittaranjan & Giese, Holger