Grundlagen heterogener Spezifikationen mittels Zustandsmaschinen und temporaler Logik

• Antragsteller: Professor Dr. Gerald Lüttgen, seit 5/2020
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2013 bis 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 233929853

Formalismen zur Spezifikation nebenläufiger Systeme, welche Zustandsmaschinen mit logischen Operatoren kombinieren, erlauben prägnantere Spezifikationen. Ziel dieses Projekts ist die Verbesserung der theoretischen Grundlagen und der Anwendbarkeit solcher Formalismen und insbes. von Interface-Theorien. Dazu wurde in diesem Projekt auf der Basis der Interface-Automaten von de Alfaro und Henzinger und der modalen Transitionssysteme von Larsen et al. die MIA-Theorie (Modal Interface Automata) entwickelt. Im Gegensatz zu verwandten Arbeiten und unter Beibehaltung einer optimistischen Sicht auf Komponentenkompatibilität ist die MIA-Theorie nichtdeterministisch, behandelt Konjunktion und internes Verhalten angemessen und erlaubt ein wirklich kompositionelles Verfeinern von Interfaces. Zudem wurde MIA auch um temporallogische Operatoren zur Spezifikation von Sicherheitseigenschaften erweitert, so dass eine wahrhaftig heterogene Spezifikationstheorie entstanden ist.Die hier beantragte Fortsetzung des Projekts soll MIAs Heterogenität und Praktikabilität in dreierlei Hinsicht verstärken. Erstens soll der MIA-Ansatz für die Behandlung von Lebendigkeits- und Fairnesseigenschaften ergänzt und dazu mit einer ausgefeilteren Verfeinerungsrelation ausgestattet werden. Zweitens soll MIAs Kommunikationsmechanismus um Datenübermittlung via Value Passing und Shared Variables erweitert werden, die beide in modernen parallelen Programmiersprachen zu finden sind. Drittens soll MIA als Typsystem für die Programmierung paralleler, komplexer Systeme verwendet und entsprechend zu einer Theorie von Verhaltenstypen angepasst werden; bislang wurde es ausschließlich als eine Verfeinerungstheorie zur Unterstützung des modellgetriebenen Entwurfs konzipiert. Das Projektergebnis werden neue und ausdrucksstarke Interface- und Verhaltenstyp-Theorien sein, die von prototypischen Software-Werkzeugen für Googles parallele Programmiersprache Go begleitet und mithilfe von Fallstudien evaluiert werden.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Finnland, USA
• Kooperationspartner: Professor Rance Cleaveland, Ph.D.; Professor Dr.-Ing. Uwe Nestmann; Professor Antti Valmari
• Ehemaliger Antragsteller: Professor Dr. Walter Vogler, bis 5/2020