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

Eingebettete Systeme sind heutzutage allgegenwärtig. Eine große Herausforderung für die Softwareentwicklung von eingebetteten Systemen stellt die hohe Komplexität der Systeme dar. Refactoring ist in der modellbasierten Entwicklung ein etabliertes Verfahren, um mittels Modelltransformationen die Komplexität der Modelle zu reduzieren und Modelle in Einklang mit Standards zu bringen. Dies ist insbesondere in sicherheitskritischen Umgebungen von besonderer Bedeutung. In sicherheitskritischen Bereichen spielt zudem formale Verifikation eine große Rolle. Die zentrale Eigenschaft, die es für ein Refactoring zu garantieren und ggf. formal zu verifizieren gilt, ist die Verhaltensäquivalenz von Quell- und Zielmodell.Das Ziel des geplanten DFG-Projekts KorMoran III ist es, Verifikationsmethoden für die Verhaltensäquivalenz von Quell- und Zielmodell von graphbasierten Modellen zu entwickeln. In KorMoran I und II haben wir bereits Transformationen auf graphbasierten Modellen untersucht, deren Semantik über einen logischen Zeitbegriff verfügt. In KorMoran II haben wir außerdem begonnen, auch Transformationen auf Modellen mit einem metrischen Zeitbegriff zu untersuchen. Diese Untersuchungen sollen nun in KorMoran III fortgeführt werden. Dazu sollen zunächst Verifikationstechniken für rein zeitdiskrete und -kontinuierliche Datenflussmodelle untersucht werden. Anschließend sollen beide Paradigmen kombiniert werden, um eine Theorie für zeit-hybride datenflussorientierte Modelle zu entwerfen. Darüber hinaus planen wir, einen Kompositionalitätsbegriff für hybride Datenflussmodelle zu entwickeln. Wir planen zudem eine Methodik, die verhaltensäquivalente Refactorings für gegebene Modelle automatisch vorschlägt. Da wir insbesondere industrielle Anwendungen unterstützen möchten, beziehen wir die Forschung auf eines der bedeutendsten Werkzeuge für modellbasierte Entwicklung in der Automobil-, Luftfahrt- und Schienenverkehrsindustrie, nämlich auf MATLAB/Simulink. Diese Arbeiten zur Verifikation von Modelltransformationen auf Datenflussmodellen sollen von der TUB fortgeführt werden.Darüber hinaus planen wir, die Theorie für zeit-hybride Modelle mit bereits in KorMoran I und II entwickelten Techniken für Transformationen mit logischem Zeitbegriff zu kombinieren. Das Ziel ist es, Verhaltensäquivalenz für Modelle, die sowohl datenflussorientierte Anteile als auch automatenähnliche Anteile enthalten, zeigen zu können. Um auch hierfür die industrielle Anwendbarkeit sicherzustellen, sollen die Methoden auf Simulink (für den Datenflussanteil) und Stateflow (für den Automatenanteil) angewandt werden. TUB und HPI werden diesen Teil gemeinsam entwickeln.

• DFG-Verfahren: Sachbeihilfen