Temporal Logic Sketching: ein computergestützter Ansatz zum Erstellen formaler Spezifikationen

• Antragsteller: Professor Dr. Daniel Neider
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2020 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 434592664

Die Entwicklung moderner Systeme erfordert ein gutes Verständnis der Spezifikationen, die das System erfüllen soll. Dieses Verständnis in vollständige und korrekte Spezifikationen zu übersetzen, ist jedoch komplex und fehleranfällig. Wesentliche Eigenschaften werden leicht übersehen und oft ist der Aufwand, formale Spezifikationssprachen zu erlernen, größer als der erwartete Nutzen.Dieser Antrag soll Antworten auf die grundlegende Frage liefern, wie das intuitive Verständnis eines Entwicklers von einem komplexen System in eine formale Spezifikation übersetzt werden kann. Das Ziel ist die Entwicklung eines neuartigen, computergestützten Ansatzes zum Schreiben formaler Spezifikationen, genannt "Temporal-Logik-Sketching", sowie dessen Implementierung als Open-Source-Software. Dieser Ansatz wird einem Entwickler die Möglichkeit geben, Anforderungen an ein System als eine partielle Spezifikation (als "Sketch") zu formulieren, bei dem schwer zu spezifizierende Aspekte ausgelassen werden können. In Interaktion mit dem Entwickler, z. B. durch den Austausch von Beispielen, synthetisiert anschließend ein "Sketching-Tool" die vollständige Spezifikation, die der Entwickler im Sinn hatte. Darüber hinaus wird der Sketching-Ansatz die Option bieten, Spezifikationen automatisch mit für die Praxis wichtigen Eigenschaften wie Robustheits- und Qualitätsgarantien anzureichern.Dieses Projekt konzentriert sich auf vier Spezifikationssprachen, die als De-facto-Standard zur Spezifikation temporaler Eigenschaften im Bereich der Verifikation und Synthese gelten (daher der Name "Temporal-Logik-Sketching"): Linear Temporal Logic (LTL), Computational Tree Logic (CTL), CTL* und Signal Temporal Logic (STL). Dabei hat dieses Projekt drei Hauptziele:1) Ausgehend von unserer Vorarbeit zum Lernen von LTL-Formeln werden wir effektive Lernalgorithmen für die vier genannten Logiken entwickeln. Mittels mathematischer Optimierung werden wir sicherstellen, dass die gelernten Formeln leicht von Menschen zu verstehen sind. Interpretierbarkeit ist wesentlich für dieses Projekt, wird aber im Bereich des maschinellen Lernens erst seit Kurzem untersucht.2) Wir werden die theoretischen Grundlagen des Temporal-Logik-Sketching entwickeln und als Software-Tool implementieren. Ähnlich zu unseren Arbeiten im Bereich der lernbasierten Verifikation werden wir dabei induktive Techniken (d. h. die genannten Lernalgorithmen) und deduktive Techniken (aus dem Bereich Logik) kombinieren.3) Wir werden Erweiterungen von LTL, CTL, CTL* und STL entwickeln, die Robustheits- und Qualitätsgarantien standardmäßig berücksichtigen. Dies werden wir durch den Schritt von einer Booleschen zu einer mehrwertige Semantik erreichen.Wir sind überzeugt, dass das Prinzip des Temporal-Logik-Sketching das Erstellen von Spezifikationen, auch über temporale Logiken hinaus, stark vereinfachen wird. Dadurch entfällt eines der größten Hindernisse für eine weitere Verbreitung formaler Methoden in der Praxis.

• DFG-Verfahren: Sachbeihilfen