Datengetriebene Safety-Spezifikation mittels Contract Mining

Kontext 

Cyber-physische Systeme werden oft in sicherheitskritischen Umgebungen eingesetzt, beispielsweise in Autos, Flugzeugen oder medizinischen Geräten. 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 im Betrieb bewährten Systeme nun in einer sicherheitskritischen Funktion eingesetzt werden sollen, müssen sie ebenfalls neu mit Contracts spezifiziert werden. 

Diese Masterarbeit soll sich der Frage widmen: Geht das auch anders? Automatisiert? Verschiedene Publikationen haben gezeigt, dass datenbasiert mithilfe von neuronalen Netzen, 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

• Recherche zu neuen Verfahren und Werkzeugen zum Mining von STL-Spezifikationen und anderen temporalen Logiken
• Konzeption und Implementierung eines geeigneten Mining-Verfahrens
• Evaluation und Vergleich der umgesetzten Methode mit Verfahren aus der Literatur anhand verschiedener Test-Systeme

Voraussetzungen

• Interesse an Data mining, maschinellem Lernen, funktionaler Sicherheit und formalen Methoden 
• Fundierte Programmierkenntnisse (Python/C++)
• Zuverlässige und eigenständige Arbeitsweise