Reactive Synthesis of Graphical User Interface Program Code
Final Report Abstract
Programs with a graphical interface (GUI) are difficult to get right. Such programs respond to events such as button clicks and network accesses finishing by changing the state of the user interface and starting new computation threads. Due to the user’s behavior and the order of events being unpredictable, developers of GUI programs often forget cases, leading to incorrect programs. In this project, we addressed this difficulty by developing the necessary theory and tools to lift the idea of automatically synthesizing an implementation to the realm of graphical user interface glue code. Starting point was the observation that the particular properties of GUI synthesis as an application domain can be exploited to make the synthesis process more efficient. The specification governing how the user interface behaves tends to be relatively simple in this setting and describes chains of events that may or may not happen, which allows to utilize a relatively restricted type of technical representation for the specification, called universal very-weak omega-automata. Such automata consist of states that represent obligations that the GUI program code has to fulfill. Furthermore, events and actions do not happen in parallel in GUIs and can be assumed to occur sequentially, where the GUI program code can react to every input event with multiple actions. These two observations can be exploited in a synthesis process that uses a synthesis game that encodes the interaction between the user and the program. In this game, only the best-case sequences of actions of the system need to be considered, where what is best is defined in terms of the obligations. This approach enabled building small synthesis games with a so-called Generalized Reactivity(1) winning condition, which was already known in the literature. To achieve and support these results, a couple of questions with a more theoretical focus also had to be answered. This includes defining a sub-logic of linear temporal logic (LTL) useful for describing GUI properties that is tailored towards a translation to universal very-weak automata. Similarly, we researched an approach to finding so-called invariants implied by a specification in generalized reactivity(1) synthesis, which helps a system designer with identifying which system behavior a specification implies and hence with debugging a given specification. To maintain the efficiency of generalized reactivity(1) synthesis, as used in our GUI code synthesis approach, while allowing some more complex specification parts, we furthermore provided a new synthesis approach that bridges generalized reactivity(1) synthesis with synthesis from full LTL. The new approach bases on a novel canonical form for arbitrary omega-regular specifications, which was also found in the scope of the project.
Publications
-
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
