Reaktive Synthese von Programmcode für Grafische Benutzeroberflächen

• Antragsteller: Professor Dr. Rüdiger Ehlers
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2016 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 322591867

Programme mit einer grafischen Benutzeroberfläche (GUI) durchlaufen oft viele Entwicklungszyklen, bevor das Interaktionsschema zwischen dem Programm und dessen Benutzer finalisiert ist. Der GUI-Bindecode, der das Verhalten der Benutzeroberfläche mit dem sogenannten Back-End koordiniert, muss dabei mehrmals aktualisiert werden, was nicht nur Entwicklerzeit kostet, sondern auch die Fehleranfälligkeit des Programmcodes erhöht.Das Synthetisieren des GUI-Bindecodes löst dieses Problem. In der ersten Förderphase des Projektes wurde ein äußerst skalierbarer spielbasierter Synthesealgorithmus speziell für GUI-Bindecode entwickelt. Die Umgebungsannahmen und Programmanforderungen werden dabei als universelle sehr schwache Büchi-Automaten repräsentiert, die eine natürliche Ordnung der Spielpositionen bzgl. der zu erfüllenden Aufgaben durch das System induzieren. Dies wurde mit einer Ausführungssemantik kombiniert, in der GUI-Bindecode auf jedes Ereignis mit mehreren Aktionen reagieren kann. Diese Semantik ist nicht nur besser für diesen Anwendungsbereich geeignet, sondern führt auch zu einer substanziellen Verkleinerung der Spielgröße, wenn nur Spielteile betrachtet werden, die optimales Verhalten des Systems bzgl. der natürlichen Ordnung der Spielpositionen repräsentieren. Dadurch beschleunigt sich verglichen mit anderen aktuellen Syntheseverfahren für allgemeine reaktive Systeme der Syntheseprozess um mehreren Größenordnungen.Der neue Syntheseansatz verlagert zugleich die Schwierigkeit des Syntheseproblems vom Lösen eines großen Synthesespiels zur Konstruktion eines relativ kleinen Synthesespiels. Dies ist eine neue Situation in der Forschung an der reaktiven Synthese, in der das Hauptproblem bisheriger Ansätze in der Regel ist, dass die zu lösenden Spiele zu groß sind, um sie mit den bekannten Spiellösealgorithmen und begrenztem Speicher zu bearbeiten. In der zweiten Projektphase wird auf der kleinen Spielgröße bei Nutzung des neuen Syntheseansatzes aufgebaut. Startpunkt ist eine Methode, um eine Repräsentation der sinnvollen Aktionssequenzen des GUI-Bindecodes direkt aus der Spezifikation zu berechnen, so dass nur diese bei der Konstruktion des Spiels betrachtet werden müssen. Die resultierende Effizienzsteigerung wird von einem neuen Ansatz zur Berechnung von Invarianten der synthetisierten Strategie komplementiert. Diese Invarianten zeigen auf, wie die synthetisierte Strategie die langfristige Erfüllung der Spezifikation und die Maximierung der Verfügbarkeit von GUI Elementen kombiniert.Beide algorithmischen Neuerungen sind elementar, um die Synthese in industrielle Entwicklungsprozesse zu integrieren, da zum einen dort sehr große GUI-Spezifikationen bearbeitet werden müssen, und zum anderen das Vertrauen in die synthetisierten Implementierungen hergestellt werden muss.

• DFG-Verfahren: Sachbeihilfen