Reaktive Synthese von Programmcode für Grafische Benutzeroberflächen
Zusammenfassung der Projektergebnisse
Die Entwicklung von Programmen mit grafischer Benutzeroberfläche (GUI) ist schwierig. Solche Programme reagieren auf Ereignisse wie Klicks oder der Ankunft von Daten aus dem Netzwerk, indem der GUI-Zustand geändert wird und neue Berechnungen gestartet werden. Weil das Nutzer-Verhalten sowie die Reihenfolge der Ereignisse schwer vorhersagbar sind, vergessen Entwickler solcher Programme oft Fälle, was zu fehlerhaftem Programmverhalten führt. In diesem Projekt wurden Theorie und Tools entwickelt, um die Idee der automatischen Synthese von Programmcode in den Anwendungsbereich der grafischen Benutzeroberflächen zu heben. Ausgangspunkt war die Beobachtung, dass die besonderen Eigenschaften von GUI Programmcode genutzt werden können, um den Syntheseprozess effizienter zu gestalten. Spezifikationen, die definieren, wie sich Benutzeroberflächen verhalten, sind oft relativ simpel und beschreiben Sequenzen von Ereignissen. Diese können auf technischer Ebene als eine besondere Form von Automaten, genannt universelle sehr schwache Omega-Automaten, darstellt werden, in denen die Zustände Anforderungen an den weiteren Verlauf der Interaktion darstellen. Weiterhin können Ereignisse und Aktionen in GUIs nicht parallel stattfinden, wobei der GUI Programmcode auf jedes Ereignis mit mehreren Aktionen reagieren darf. Beide Beobachtungen können genutzt werden, wenn das Synthese-Problem auf das Lösen eines Spieles zwischen dem GUI Programmcode und dessen Benutzer reduziert wird. Dabei müssen nur die bestmöglichen Aktions-Sequenzen des Programmcodes, d.h., diejenigen, die zu möglichst geringen Einschränkungen bzgl. des zukünftigen Systemverhaltens führen, betrachtet werden. Die resultierenden kleinen Synthesespiele haben eine sogenannte Generalized Reactivity(1) Gewinnbedingung, für die Spiellösungsalgorithmen bekannt sind. Zum Erreichen und zur Unterstützung dieser Resultate mussten ein paar zusätzliche Forschungsfragestellungen bearbeitet werden. Dies beinhaltet die Entwicklung einer Unterlogik von Linear Temporal Logic (LTL), die für die Beschreibung von GUI-Eigenschaften nützlich ist und eine direkte Übersetzung in universelle sehr schwache Automaten hat. Ebenso wurde ein Ansatz erforscht, der Invarianten findet, die durch eine Spezifikation für die Generalized Reactivity(1) Synthese impliziert werden. Dies hilft einem Entwickler, das Verhalten des synthetisierten Systems zu verstehen und Fehler in der Spezifikation zu finden. Um die Effizienz der Generalized Reactivity(1) Synthese (wie sie in unserem GUI Programmcode Synthese Ansatz verwendet wird) beizubehalten, aber dennoch auch komplexere Spezifikationsteile unterstützen zu können, wurde weiterhin ein neuer Synteseansatz entwickelt, der die Stärken dieses Syntheseansatzes mit der vollständigen Unterstützung von LTL kombiniert. Der Ansatz basiert auf einer neuen kanonischen Normalform für Omega-reguläre Sprachen, die im Rahmen des Projektes ebenfalls entwickelt wurde.
Projektbezogene Publikationen (Auswahl)
-
A Fragment of Linear Temporal Logic for Universal Very Weak Automata. Lecture Notes in Computer Science, 335-351. Springer International Publishing.
Adabala, Keerthi & Ehlers, Rüdiger
-
Approximately Propagation Complete and Conflict Propagating Constraint Encodings. Lecture Notes in Computer Science, 19-36. Springer International Publishing.
Ehlers, Rüdiger & Palau, Romero Francisco
-
How Hard Is Finding Shortest Counter-Example Lassos in Model Checking?. Lecture Notes in Computer Science, 245-261. Springer International Publishing.
Ehlers, Rüdiger
-
Reactive Synthesis of Graphical User Interface Glue Code. Lecture Notes in Computer Science, 387-403. Springer International Publishing.
Ehlers, Rüdiger & Adabala, Keerthi
-
„Natural Colors of Infinite Words“. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS). Vol. 250. LIPIcs.
R. Ehlers & S. Schewe
-
Fully Generalized Reactivity(1) Synthesis. Lecture Notes in Computer Science, 83-102. Springer Nature Switzerland.
Ehlers, Rüdiger & Khalimov, Ayrat
-
Understanding Synthesized Reactive Systems Through Invariants. Lecture Notes in Computer Science, 170-187. Springer Nature Switzerland.
Ehlers, Rüdiger
