Beweisberücksichtigende Entwicklung von Cyber-physischen Systemen

Motivation Cyber-physische Systeme (CPS) werden in vielen sicherheitskritischen Bereichen, wie Straßenverkehr und Luftfahrt, eingesetzt in denen Menschenleben auf dem Spiel stehen. Eine unabdingbare Voraussetzung für die Entwicklung korrekter CPS ist eine genaue Analyse ihres Verhaltens, welches eine Kombination von diskreter Dynamik (cyber-Teil, z.B. Beschleunigung eines Autos festlegen) mit stetiger Dynamik (physischer-Teil, z.B. Bewegung des Autos) darstellt. Deshalb sind formale Verifikationstechniken von höchster Wichtigkeit um ordnungsgemäßes Verhalten in den unendlich vielen möglichen Zuständen eines CPS zu garantieren nicht nur in manchen, wie bei Simulation oder durch Testen. Problem Formale Verifikation basiert auf Modellen zur Beschreibung der unendlich vielen Zustände dieser CPS. Aktuelle Methoden sind meist ein Kompromiss zwischen vollständiger Automatisierung und Ausdrucksmächtigkeit der Modellierungssprache: Erreichbarkeitsanalyse fokussiert auf volle Automatisierung und beschränkt dafür die Expressivität der Modelle, während deduktive Beweismethoden auf Benutzersteuerung angewiesen sind, aber im Gegenzug realitätsnähere Modelle erlauben. Um trotz der inhärenten Komplexität von CPS die Steuerung durch Benutzer zu ermöglichen ist inkrementelle Entwicklung unumgänglich. Mit aktuellen Verifikationsmethoden ist dabei jedoch nach jeder Iteration eine vollständig Re-verifikation des Modells notwendig. Gleichzeitig sollen die formal verifizierten Korrektheitsgarantien des Modells auch für die eigentliche Implementierung gelten. Um das zu gewährleisten gilt es die Kluft zwischen Modellierungskonzepten (z.B. nicht-deterministische Steuerungen) und Implementierungskonzepten (z.B. deterministische Befehle) entsprechend zu schließen. Die Vision diese Projekt ist, den Verifikationsaufwand trotz inkrementeller Entwicklung von CPS zu minimieren und gleichzeitig Korrektheitsaussagen über Modelle auf die Implementierung zu übertragen. Herausforderungen Um dieser Vision näher zu kommen werden wir basierend auf unserer bisherigen Erfahrungen mit CPS Konzepte, Methoden, Techniken und Werkzeuge zur inkrementellen und beweisberücksichtigenden Entwicklung von CPS bereitstellen. Beweisberücksichtigende Verfeinerung: Entwicklung beweisbarkorrekter Verfeinerungsoperationen um die Struktur (z.B. duplizierte Kontrollentscheidungen teilen) oder das Verhalten (z.B. Sensorunsicherheit einführen) eines Modells zu verändern und automatische Ableitung von Bedingungen, die verifiziert werden müssen, um Korrektheit weiterhin zu garantieren. Beweisberücksichtigende Komposition:Entwicklungvonbeweisbarkorrekten Kompositionsoperationen um verifizierte CPS Komponenten zu verbinden, automatische Ableitung von Bedingungen die verifiziert werden müssen um die Gesamtsicherheit des Systems zu garantieren und Komponenten an ihre neue Umgebung anzupassen. Beweisberücksichtigende Implementierung: Entwicklung von beweisbar korrekten Transformationsoperationen (z.B. nicht-deterministische Sensordaten durch Sensorzugriffe ersetzen) die CPS Modelle automatisch in Code umwandeln. Evaluierung Der von der geplanten Forschung zu erwartende Nutzen umfasst verminderten Aufwand bei Modellierung, Verifikation und Implementierung von CPS und erhöhte Korrektheit von Implementationen. Wir planen die Umsetzbarkeit des Ansatzes mit Fallstudien aus den Bereichen Straßenverkehr und Robotik zu demonstrieren.

Cyber-physische Systeme kommen in sicherheitskritischen Bereichen, wie Straßenverkehr und Luftfahrt, zum Einsatz und benötigen daher genaueste Korrektheits-Analysen mit rigorosen Sicherheits-Garantien. Das Projekt ProoAwareCPS entwickelte Modellierungs- und Beweistechniken, mit denen cyber-physische Systeme aus mathematisch bewiesen korrekten Teilkomponenten derartig zusammengesetzt werden können, dass daraus bewiesen korrekte Systemfunktionalität folgt. Cyber-physische Systeme zeichnen sich durch eine stark verwobene Interaktion zwischen computerbasierten Entscheidungen (z.B. ob und wann ein selbstfahrendes Auto bremsen muss oder beschleunigen darf, und wie es Lenkeinschlag zu wählen hat) und dem durch diese Entscheidungen bedingten physischen Verhalten (z.B. die Bewegung des Fahrzeuges selbst) in Relation zu anderen Teilehmern in der Umgebung (z.B. das Verhalten von Fussgängern) aus. Besondere Herausforderung im Projekt war die umfassende Behandlung dieses hybriden software-gesteuerten physischen Verhaltens und die Projektergebnisse umfassen insbesonders nicht nur die Kontroll-Entscheidungen der Software sondern auch das physische Verhalten. Als grundlegende Eckpfeiler des Ansatzes wurden im Projekt drei Themen bearbeitet: beweisberücksichtigende Komposition, beweisberücksichtigende Verfeinerung, und beweisberücksichtigende Implementierung. Beweisberücksichtigende Komposition greift auf im Projekt ausgearbeitete Schablonen für die Beschreibung von Komponenten und deren Zusammenarbeit zurück, und beschreibt Beweise die in automatisierter logik-basierter Analysesoftware (Theorembeweiser für cyber-physische Systeme) umgesetzt sind. Beweisberücksichtigende Verfeinerung beschreibt Techniken zur inkrementellen Entwicklung von Komponenten und kommt insbesondere in den im Projekt ausgearbeiteten, allgemeingültigen Beweisen, zum Einsatz. Beweisberücksichtigende Implementierung stellt Techniken zur Übersetzung von Komponenten-Modellen in ausführbare Steuerungs- und System-Überwachungssoftware in einer gängigen Programmiersprache zur Verfügung. Durch die Projektergebnisse wird die verteilte modellbasierte Entwicklung von cyber-physischen Systemen mit Sicherheitsgarantien wesentlich unterstützt. Die entwickelten Beweistechniken wurden im Rahmen von Modellierungs- und Beweisstudien zu den Themen Verkehrsfluss-Analyse und Kollisionsvermeidung in der Robotik demonstriert.