Hasso-Plattner-Institut
Prof. Dr. Holger Giese
  
 

Korrekte Modelltransformationen

Eingebettete Systeme sind heutzutage allgegenwärtig. Durch immer größer werdende Rechenleistungen und Vernetzung der Systeme sind diese in der Lage, immer komplexere Aufgaben zu erfüllen. Um diese Komplexität beherrschen zu können, ist es notwendig, standardisierte und bewährte Methoden der Softwareentwicklung anzuwenden. Dazu zählt die modellgetriebene Entwicklung (MDE), die den Entwickler beim Design der abstrakten Anwendungsfälle bis zum konkreten, ausführbaren Code begleitet. Auch die abstrakten Modelle können sehr komplex werden. Eine Technik zur Reduzierung der Komplexität ist das Refactoring - Modelltransformationen, die äquivalentes Verhalten bei Ausführung der Modelle garantieren. In besonders sicherheitskritischen Bereichen, beispielsweise in der Automobil-, Luftfahrt- und Schienenverkehrsindustrie, spielt darüber hinaus formale Verifikation eine große Rolle. In diesen Industriezweigen wird zum MDE überwiegend MATLAB/Simulink eingesetzt.

Das DFG-Projekt KorMoran widmet sich daher dem Problem der Verifikation von Modelltransformationen, konkret dem formalen Beweis der Verhaltensäquivalenz von Quell- und Zielmodell. In den Vorgängerprojekten KorMoran I und II wurden sowohl Transformationen für zeit-diskrete und wert-diskrete Transitionsmodelle als auch für zeit-diskrete, zeit-kontinuierliche und wert-kontinuierliche Datenflussmodellen untersucht. In KorMoran III sollen nun zunächst die Untersuchungen zu zeit-diskreten und zeit-kontinuierlichen Datenflussmodellen fortgesetzt werden. Insbesondere ist eine Erweiterung der Verifikationsmethoden geplant, um hybride Systeme zu unterstützen - Modelle also, in denen sowohl zeit-diskrete als auch zeit-kontinuierliche Anteile gemischt vorkommen.

Bezüglich der Verifikation von Transformationen für Transitionsmodelle sollen Erweiterungen bestehender Techniken bezüglich der Ausdrucksmächtigkeit und Anwendbarkeit unternommen werden. Konkret sollen die existerienden Verifikationstechniken erweitert werden, um neben Bisimulation und Simulation auch schwache Bisimulation und Simulation zu untersützen. Zusätzliche sollen auch Methoden für Transformationen für Transitionsmodelle mit wert-kontinuierlichen Signalen entwickelt werden.

KorMoran III ist ein Kooperationsprojekt zwischen der Technischen Universität Berlin und dem Hasso-Plattner-Institut, wobei erstere den Fokus auf den Bereich der Datenflussmodelle legt, während Modelltransformationen für Transitionsmodelle am Hasso-Plattner-Institut betrachtet werden. Gemeinsamer Teil des Projekts wird die Kombination entwickelter Techniken sein, um Anwendbarkeit für in Datenflussmodelle eingebettete Transitionsmodelle zu untersuchen und zu erreichen.

Projektpartner

Projektförderung

Dieses Projekt wird finanziert durch die DFG.

Dauer der Förderung (Kormoran):

Anfang: 01.01.2010

Ende: 31.12.2012


Dauer der Förderung der Fortsetzungsphase (KorMoran II):

Anfang: 01.08.2013

Ende: 30.09.2016


Dauer der Förderung der zweiten Fortsetzungsphase (KorMoran III):

Anfang: 01.11.2017

Ende: 31.10.2018

Publikationen