Datengetriebene Safety-Spezifikation mittels Large Language Models

Kontext 

Cyber-physische Systeme werden oft in sicherheitskritischen Umgebungen eingesetzt, beispielsweise in Autos, Flugzeugen oder medizinischen Geräten. Die Gewährleistung der (funktionalen) Sicherheit bzw. Safety ist daher eine zentrale Aufgabe in der Entwicklung der Systeme. Eine formale Spezifikation, die die Garantien und Annahmen des Systems definiert, ist für diesen Zweck besonders wichtig. Für cyber-physische Systeme eignet sich besonders die Signal Temporal Logic (STL) als formale Beschreibungssprache. Leider bringt diese Methodik zusätzlichen Aufwand in der Entwicklung mit sich: zu jeder Komponente wird eine Spezifikation in STL benötigt, die bisher händisch erstellt werden muss. 

Diese Masterarbeit soll sich daher der Frage widmen: Wie kann man die Formalisierung einer Komponente in STL automatisieren? Wie können wir aus aufgezeichneten Daten des Systems seine Spezifikation bestimmen? Diverse Publikationen haben gezeigt, dass datenbasiert mithilfe genetischer Algorithmen, Decision Trees oder Clusteringverfahren Contracts abgeleitet werden können. Der hier zu untersuchende Ansatz zielt stattdessen darauf ab, ein Large Language Model (LLM) für die automatische Erstellung der formalen Beschreibung in STL zu nutzen. LLMs haben in verschiedenen Anwendungsdomänen herausragende Ergebnisse in der Generierung von Texten gezeigt. Die zentrale Frage der Masterarbeit ist daher, wie man einem LLM beibringt, aus Signalen (Zeitreihen) einen Text in formaler Sprache zu generieren.

Ziele

• Recherche zur Anwendung von LLMs auf Zeitserien, wie Prompting, Quantisierung und Alignment mit Sprache
• Konzeption und Implementierung eines geeigneten Verfahrens
• Erstellung eines Datensatzes zum Training und Auswertung des Verfahrens
• Evaluation der umgesetzten Methode 

Voraussetzungen

• Interesse an LLMs, funktionaler Sicherheit und formalen Methoden (STL)
• Fundierte Programmierkenntnisse (Python)
• Zuverlässige und eigenständige Arbeitsweise