Formale Methoden für Contracting

• Antragstellerin: Professorin Dr.-Ing. Ina Schaefer
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung von 2013 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 206480214

Die Einführung standardisierter Hardwareabstraktionsschichten und Laufzeitumgebungen für die Anwendungsentwicklung (z.B. AUTOSAR im Automotive Bereich) erlauben es flexible Softwareinfrastrukturen zu schaffen. Durch die Kommunikation mit anderen Geräten und das Nutzen von nicht immer erreichbarer Geräte als dynamische Ressourcen, nimmt die Flexibilität zukünftiger, aber auch aktueller Anwendungen für eingebettete Systeme immer weiter zu. Diese Vernetzung und Kommunikation führt zudem dazu, dass die Kontrolle über ein eingebettes Softwaresystem nicht mehr unbedingt zentral, sondern auch durch andere Geräte ausgeführt werden kann. Durch die weitgehend unabhängige Entwicklung von Anwendungen, Laufzeitumgebung (Betriebssystem) und Plattform steigt auch die Nachfrage nach Methoden, welche es erlauben diese Komponenten nach der Inbetriebnahme weitgehend unabhängig voneinander weiterzuentwickeln. Im Rahmen der CCC Forschergruppe soll Projekt B2 einen Kontraktformalismus und entsprechende Methoden entwickeln, die es erlauben zur Laufzeit eines Systems Komponenten nachträglich zu modifizieren und zu integrieren. Der Kontraktformalismus soll zudem in der Lage sein, sich Gegebenheiten wie offenen Netzwerken, sich dynamisch ändernden Plattformen und verteilten, dezentralen Kontrolle anzupassen. Dies verlangt flexible Kontraktschnittstellen zwischen Anwendungen, Middleware und Plattform. Des Weiteren werden formal verifizierte Kontraktverhandlungsmechanismen für das Hinzufügen und Verändern von Kontrakten benötigt. Hierbei dürfen auch Optimierungsprobleme nicht vernachlässigt werden. Da Ressourcen auch für die Kontraktverhandlung auf eingebetteten Systemen sehr limitiert sind, ist es notwendig den Verbrauch eben dieser zu minimieren. Es müssen daher schon vorhandene Ergebnisse vorhergegangener Verhandlungen wieder verwendet werden. Hierfür werden wir untersuchen, für welche Klasse von Eigenschaften eine inkrementelle Verhandlung sinnvoll ist und wie sie funktionieren kann. Ergebnisse in eingebetteten Systemen sind immer mit einer Unsicherheit, vor allem in Verbindung mit Sensoren, verbunden. Wir werden daher die Auswirkungen von Unsicherheit auf Kontraktverhandlungen untersuchen. Im Detail beschäftigt sich dieses Projekt mit (1) der Entwicklung eines Kontraktformalismus, welcher mehrere Klassen von Eigenschaften (Sicherheit, Verfügbarkeit und funktionale Korrektheit) umfasst, und gleichzeitig die Spezifika von Anwendungsanforderungen und Plattformeigenschaften berücksichtigt; (2) der Entwicklung eines vollständigen Kontraktmechanismus mit verschiedenen Analysen für jede Klasse von Eigenschaften (3) nicht nur unter Berücksichtigung von Anforderungserfüllung, sondern auch von Parameteroptimierung des Systems unter Berücksichtigung der Kontrakte; (4) der Entwicklung von kompositionellen und inkrementellen Methoden um die Effizienz des Kontraktmechanismus zu steigern.

• DFG-Verfahren: Forschungsgruppen
• Teilprojekt zu: FOR 1800: Überwachung und Steuerung nebenläufiger Funktionsänderungen in kritischen Systemen
• Internationaler Bezug: Frankreich
• Kooperationspartnerin: Sophie Quinton, Ph.D.