Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

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 2024
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 233929853
 
Erstellungsjahr 2024

Zusammenfassung der Projektergebnisse

Reaktive Systeme erfassen kontinuierlich ihre Umgebung und berechnen Reaktionen, die diese Umgebung beeinflussen. Die komponentenbasierte Software solcher Systeme implementiert nebenläufige Zustandsautomaten und wird oftmals abstrakt mittels Aussagen- und Temporallogik spezifiziert. Der Entwurf reaktiver Systeme erfordert daher heterogene Modellierungssprachen, die logische und operative Paradigmen verbinden. Um Eigenschaften von nebenläufigen Komponenten zu bestimmen, ist zudem eine kompositionelle Verfeinerungsordnung wünschenswert, die sensitiv bzgl. Deadlock und Kommunikationsfehlern ist. Ausgangspunkt des Projekts waren Interfacetheorien auf Grundlage der Interface-Automaten (IA) von de Alfaro und Henzinger und Spezifikationstheorien auf Basis der modalen Transitionssysteme (MTS) von Larsen. Diese erweitern nebenläufige Zustandsautomaten und erlauben Abstraktion durch Nichtdeterminismus sowie schrittweises Verfeinern. Jedoch unterstützen sie nicht die logische Spezifikation und machen stark einschränkende Annahmen bzgl. Nichtdeterminismus, Kompositionalität und Abstraktion von internem Verhalten. Vor diesem Hintergrund sollte das Projekt Grundlagen und praktischen Nutzen heterogener Spezifikationsformalismen verbessern. Zur Erreichung dieses Ziels wurde erst das Zusammenspiel zwischen Kommunikationsfehlern, Kompositionalität und Nichtdeterminismus untersucht. Ein Kommunikationsfehler tritt auf, wenn ein gesendetes Ereignis von einer empfangenden Komponente nicht erwartet wird. Die Untersuchungsergebnisse führten zur Entwicklung der Interfacetheorie MIA (Modal Interface Automata), die Nichtdeterminismus für Aus- und Eingabeereignisse zulässt und die modale Verfeinerungsrelation von MTS derart adaptiert, dass Kommunikationsfehler berücksichtigt werden, Kompositionalität garantiert ist und bestmöglich von internen Berechnungen abstrahiert wird. Zudem wurde in MIA die Temporallogik ACTL derart eingebettet, dass Model Checking Verfeinern bedeutet und kompositionell möglich ist. Der Konjunktionsoperator erlaubt es einer Komponente, mehrere Interfaces zu erfüllen, indem sie deren Konjunktion verfeinert. Hinsichtlich der Praxistauglichkeit dieser Grundlagen wurde untersucht, inwieweit Interfacetheorien um Shared Variable-Kommunikation erweitert werden können. Für den daraus resultierenden IAM- Formalismus (Interface Automata with shared Memory) –und auch für MIA– wurde ein Toolset bestehend aus einem Editor, einem Simulator und einem Verfeinerungschecker entwickelt. Darüber hinaus wurde eine formale Semantik für die am DLR entworfene, modellgetriebene Sprache Virtual Satellite (VirSat) definiert, welche logische Constraints zur Synchronisation von Zustandsautomaten verwendet. Die Entwicklung reaktiver Software mittels VirSat wird nun zudem durch eine kompositionelle Verfeinerungsrelation formal unterstützt.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2025 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung