Automatisierte Synthese von Programmausdrücken (AutoSynth)
Zusammenfassung der Projektergebnisse
Oft liegt die Ursache von Programmierfehlern darin, dass in einem eigentlich korrekten Algorithmus kleinere Fehler in Programmausdrücken gemacht werden. Man spricht hier oft von ±1-Fehlern, da die Ausdrücke „fast“ richtig sind und eine Schleife z.B. nur einmal zu viel oder zu wenig ausgeführt wird. Analog dazu wird bei reaktiven Systemen das temporale Verhalten oft um einen Takt verfehlt. Ziel dieses Projektes war es, den Entwickler von reaktiven eingebetteten Systemen bei der Bestimmung kritischer Programmausdrücke zu unterstützen. Die in diesem Projekt entwickelten Verfahren sind in der Lage, fehlende Programmausdrücke in „Programmskeletten“ automatisch so zu ergänzen, dass die zum Programm angegebenen Spezifikationen erfüllt werden. Die Programmskelette der reaktiven eingebetteten Systeme wurden dabei mit synchronen Programmiersprachen beschrieben und deren Spezifikationen in temporaler Logik verfasst. Zum Beginn des Projekts lagen in der Arbeitsgruppe bereits Compiler und Verifikationswerkzeuge für eine synchrone Sprache vor. Ferner baute das Projekt auf weiteren Vorarbeiten der automatischen „Controller-Synthese“ auf, bei der sogenannte kontrollierbare Eingaben eines Systems von einem automatisch zu generierenden Controller so mit Werten versehen werden, dass die geforderten Sicherheitseigenschaften erfüllt werden. Das Hauptproblem bei den zu Beginn des Projekts vorliegenden Arbeiten lag darin, dass die Verfahren zur Controller-Synthese deterministische Systeme voraussetzen. Die Standardverfahren zur Verifikation von temporalen Eigenschaften übersetzen diese jedoch in nichtdeterministische ω-Automaten, die daher determinisiert werden müssen. Die Determinisierung beliebiger ω-Automaten ist jedoch erheblich aufwändiger als im Falle von Automaten auf endlichen Eingaben, was den praktischen Einsatz der Verfahren stark limitiert. Ein wichtiger Durchbruch des Projekts bestand darin, diese Schwierigkeiten zu überwinden wofür gleich zwei Möglichkeiten gefunden wurden. Die erste beruht auf der „Unambiguity“ der aus temporaler Logik stammender ω-Automaten: Man kann zeigen, dass zu einer Eingabe zwar mehrere Durchläufe existieren, dass jedoch nur einer davon die Akzeptanzbedingung des Automaten erfüllt. Auf dieser Beobachtung konnten wir ein komplett neues Determinisierungsverfahren dieser ω-Automaten entwickeln, welches sich symbolisch und daher sehr effizient implementieren lässt. Das zweite Verfahren beruht auf der Darstellung temporaler Formeln als boolesche Kombination von Co-Büchi Formeln und der Entwicklung effizienter symbolischer Determinisierungsverfahren für Co-Büchi-Automaten. Ein weiteres wichtiges Ergebnis bestand darin, dass wir die von anderen Gruppen entwickelten Syntheseverfahren zur GR(1)-Synthese für unsere Zwecke anpassen konnten. Dabei handelt es sich um sehr effiziente Verfahren, die jedoch sehr eingeschränkte Akzeptanzbedingungen der ω-Automaten voraussetzen. Wir konnten eine sehr große Teilmenge der temporalen Logik in GR(1)-Automaten übersetzen und damit diese Verfahren zur Synthese von relativ großen Systemen erfolgreich anwenden. Wie geplant wurden außer fixpunktbasierten Verfahren, die an klassische Modellprüfungsverfahren angelehnt sind, auch deduktive Verfahren eingesetzt. Dabei haben wir die in der Förderzeit entstandenen Verfahren der „inkrementellen Induktion“ auf die Synthese von Systemen anpassen können.
Projektbezogene Publikationen (Auswahl)
- Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis. In: Montanari, A.; Napoli, M.; Parente, M. (Hrsg.): Games, Automata, Logics, and Formal Verification (GandALF) Bd. 25. Minori, Italy, 2010 (Electronic Proceedings in Theoretical Computer Science (EPTCS)), S. 89–102
Morgenstern, A.; Schneider, K.
- ALTL Fragment for GR(1)-Synthesis. In: Reich, J.; Finkbeiner, B. (Hrsg.): International Workshop on Interactions, Games and Protocols (IWIGP) Bd. 50. Saarbrücken, Germany, 2011 (Electronic Proceedings in Theoretical Computer Science (EPTCS)), S. 33–45
Morgenstern, A.; Schneider, K.
- Program Sketching via CTL* Model Checking. In: Groce, A.; Musuvathi , M. (Hrsg.): Model Checking Software (SPIN) Bd. 6823. Snowbird, Utah, USA : Springer, 2011 (LNCS), S. 126–143
Morgenstern, A.; Schneider, K.
- Synthesis of Parallel Sorting Networks using SAT Solvers. In: Oppenheimer, F. (Hrsg.): Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV). Oldenburg, Germany : OFFIS-Institut für Informatik, 2011, S. 71–80
Morgenstern, A.; Schneider, K.
- An Asymptotically Correct Finite Path Semantics for LTL. In: Bjørner, N.; Voronkov, A. (Hrsg.): Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) Bd. 7180. Mérida, Venezuela : Springer, 2012 (LNCS), S. 304–319
Morgenstern, A.; Gesell, M.; Schneider, K.
- Solving Games Using Incremental Induction. In: Johnsen, E.; Petre, L. (Hrsg.): Integrated Formal Methods (IFM) Bd. 7940. Turku, Finland : Springer, 2013 (LNCS), S. 177–191
Morgenstern, A.; Gesell, M.; Schneider, K.
