Datengetriebene Safety-Spezifikation mittels Contract Mining

Kontext

Cyber-physische Systeme werden oft in sicherheitskritischen Umgebungen eingesetzt, beispielsweise Autos, Flugzeuge oder medizinische Geräte. Die Gewährleistung der (funktionalen) Sicherheit ist daher eine sehr wichtige Aufgabe in der Entwicklung der Systeme. Auch während des Betriebs muss die Sicherheit gewährleistet werden, und Updates dürfen die Sicherheits-Garantien nicht verletzten. Eine wichtige Methode, um formal Sicherheit von Systemen zu beschreiben, sind Contracts. Ein Contract spezifiziert, welche Garantien ein System gibt, wenn bestimmte Annahmen erfüllt sind. Mit Hilfe des vertragsbasierten Entwurfs (CBD) können Systementwickler und -tester verschiedene Merkmale des Systementwurfs überprüfen. Dies sind vor allem: Zusammensetzung verschiedener Verträge, Konsistenz, Kompatibilität, und Verfeinerung. 

Leider bringt diese Methodik zusätzlichen Aufwand in der Entwicklung mit sich: zu jeder Komponente werden zusätzliche Spezifikationen benötigt, die händisch beschrieben werden müssen. Außerdem stellt sich die Herausforderung, wie wir mit alten, bereits fertig entwickelten Systemen umgehen, die bisher nicht Teil einer sicherheitskritischen Funktion waren. Wenn diese bereits im Betrieb bewährten Systeme nun in einer sicherheitskritischen Funktion eingesetzt werden sollen, müssen sie ebenfalls neu mit Contracts spezifiziert werden.

Diese Bachelorarbeit soll sich der Frage widmen: Geht das auch anders? Automatisiert? Erste Publikationen haben gezeigt, dass datenbasiert mithilfe von genetischen Algorithmen, Decision Trees oder Clusteringverfahren sinnvolle Contracts abgeleitet werden können. Der hier zu untersuchende Ansatz zielt daher darauf ab, gesammelte Daten zu nutzen, die das System in einer Simulation oder im Betrieb produziert. Für cyber-physische Systeme eignet sich besonders die Signal-temporal Logic (STL) als Beschreibungssprache für Contracts, weshalb insbesondere Mining von STL-Beschreibungen im Vordergrund steht.

Ziele

• Überblick und Recherche zu bekannten Verfahren und Werkzeugen zum Mining von STL-Spezifikationen
• Auswahl von geeigneten Tools, ggf. Implementierung eines weiteren Verfahrens
• Evaluation und Vergleich der ausgewählten Methoden anhand eines Test-Datensatzes

Voraussetzungen

• Interesse an funktionaler Sicherheit, formalen Methoden und genetischen Algorithmen 
• Fundierte Programmierkenntnisse (Python/C++)
• Zuverlässige und eigenständige Arbeitsweise