Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

Konstruktion und Verifikation eingebetteter echtzeitfähiger Steuerungssoftware und ihrer Transformation in ausführbaren Code unter besonderer Berücksichtigung von Multicore und Adaptivität

Fachliche Zuordnung Softwaretechnik und Programmiersprachen
Förderung Förderung von 2006 bis 2016
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 20128325
 
Erstellungsjahr 2019

Zusammenfassung der Projektergebnisse

Die Entwicklung eingebetteter Echtzeitsysteme, wie z.B. Flugzeuge, Autos, etc., wird zunehmend modellbasiert durchgeführt. Modelle höherer Abstraktionsebenen werden dabei schrittweise zu niedrigeren Modellebenen bis hin zum ausführbaren Code transformiert. In bisherigen Ansätzen wird die Korrektheit dieser Transformationsschritte bezüglich Sicherheits-, Lebendigkeits- und Echtzeiteigenschaften nicht garantiert. Um dieses Problem zu lösen, haben wir im Rahmen des VATES-Projekts eine Methodik zur durchgehenden computergestützten Verifikation von eingebetteten Echtzeitsystemen über alle Abstraktionsebenen hinweg entwickelt. Korrektheitsbeweise führen wir dabei sowohl in Theorembeweisern als auch in Model Checkern durch. Als Fallstudie verwenden wir das Echtzeitbetriebssystem BOSS und verschiedene selbst-adaptive Systeme, die wir in der zweiten Phase des Projekts adressieren. Auf der Modellebene betrachten wir exemplarisch den Prozesskalkül Timed CSP, der dazu geeignet ist, nebenläufige Echtzeitsysteme zu beschreiben. Um Beweise in diesem Kalkül computergestuützt, d.h. garantiert korrekt, durchführen zu können, haben wir dessen Syntax und Semantik im Theorembeweiser Isabelle/HOL formalisiert. Zur Beschreibung von Eigenschaften von Timed CSP Modellen haben wir eine zeitbehaftete Logik entwickelt. Weiterhin haben wir Bisimulationsrelationen formalisiert, mit denen Timed CSP Modelle unterschiedlicher Abstraktionsebenen formal in Beziehung gesetzt werden können. Die Verifikation mit Theorembeweisern ist üblicherweise sehr aufwändig, da Beweisschritte interaktiv vorgegeben werden müssen und nur zum Teil automatisiert werden können. Um ein Timed CSP System vor der aufwändigen, dafür aber korrekten, Verifikation im Theorembeweiser automatisiert analysieren zu können, haben wir Transformationen von Timed CSP nach Tock CSP und Timed Automata entwickelt, für die automatische Model Checker existieren. In der zweiten Projektphase haben wir selbst-adaptive Systeme betrachtet. Diese passen sich dynamisch an geänderte Umgebungen an, um ihre Systemziele bestmöglich zu erfüllen. Für deren skalierbare Verifikation haben wir einen Ansatz zur systematischen Beschreibung verteilter, selbst-adaptiver Echtzeitsysteme mit Timed CSP entwickelt. Durch unsere strikte Trennung von Adaptionsschicht und Systemschicht ermöglichen wir eine kompositionale Verifikation. Weiterhin haben wir gängige Design Patterns für die modellgetriebene Entwicklung von selbst-adaptiven Systemen in CSP formalisiert, womit die Analyse der Gemeinsamkeiten unterschiedlicher Design Patterns ermöglicht und deren Interoperabilität vereinfacht wird. Neben diesen formal rigorosen Ansätzen haben wir zusätzlich auch einen Entwicklungsansatz für selbst-lernende selbst-adaptive Systeme erarbeitet. Wir setzen dabei SystemC zur Systembeschreibung ein und integrieren Methoden des maschinellen Lernens, um die Adaptionslogik selbst dynamisch anzupassen. Die möglichen Auswirkungen dieser Anpassungen auf das System analysieren wir automatisiert mit Model Checkern für zeitbehaftete Automaten. Um (Timed CSP) Modelle höherer Abstraktionsebenen mit ausführbaren Code mechanisiert in Beziehung setzen zu können, haben wir eine generische Low-Level Sprache entwickelt und im Theorembeweiser Isabelle/HOL formalisiert. Dabei haben wir insbesondere operationale und denotationelle CSP-ähnliche Semantiken erarbeitet. Somit können formale Bezüge zwischen Modellebene und Code-Ebene über Bisimulationen und Verfeinerungsbegriffe hergestellt werden. Die wesentliche Herausforderung bei der Erstellung der Semantiken für unstrukturierte Low-Level Sprachen war dabei, diese kompositional zu entwerfen, d.h. dass einzelne Programmteile des Low-Level Programms in Isolation betrachtet werden können und Beweise über das Gesamtsystem davon abgeleitet werden können. Eine weitere Herausforderung bei dem Entwurf von Low-Level Sprachen war die Berücksichtigung der Verteilung von und der Kommunikation zwischen einzelnen Low-Level Programmen, wie es beispielsweise für Multi-Core-Systeme benötigt wird. Die Semantiken unserer Low-Level Sprache ermöglichen es uns, Code- und Modell-Ebene über Bisimulationen und formale Verfeinerungen in Beziehung zu setzen. Da sowohl Bisimulationen als auch formale Verfeinerungen Sicherheits-, Lebendigkeits-, und Echtzeiteigenschaften bewahren, können wir damit die Korrektheit zwischen Spezifikationsmodellen und implementiertem Code nachweisen. Um eine optimierte Implementierung von einem abstrakten Modell (manuell) zu erhalten, nutzen wir einen Prototyping-Ansatz, bei dem Events in CSP Prozessen an ausführbaren Code gebunden werden. Um den manuell erzeugten Low-Level Code schließlich mit Spezifikationsmodellen in (Timed) CSP in Beziehung zu setzen, haben wir zwei Ansätze entwickelt. Mit llvm2csp bieten wir die Möglichkeit, CSP Modelle aus Programmcode zu extrahieren. Diese Modelle können dann mittels der Standard-Verfeinerungsbegriffe von CSP mit den Spezifikationsmodellen in Beziehung gesetzt werden. Da die extrahierten CSP Modelle im allgemeinen sehr groß werden können, haben wir daneben einen Ansatz im Theorembeweiser entwickelt, um die Semantik des Spezifikationsmodells direkt mit dem Low-Level Code in Beziehung zu setzen. Um dies zu vereinfachen, stellen wir Hoare-Kalküle für unsere Low-Level Sprache zur Verfügung, um einzelne Beweisverpflichtungen effizienter durchführen zu können.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2024 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung