Reactive Synthesis of Graphical User Interface Program Code

• Applicant: Professor Dr. Rüdiger Ehlers
• Subject Area: Theoretical Computer Science
• Term: from 2016 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 322591867

Programs with a graphical user interface (GUI) are frequently improved in many development iterations before the interaction scheme between a program and its user is finalized. The GUI glue code that coordinates the behavior of the UI with the back end operation of the program needs to be updated each time. This not only binds developer time, but also raises the risk of introducing bugs due to unforeseen side effects of changes.Synthesizing GUI glue code solves this problem. In the first funding period of the project, we developed a highly scalable game-based synthesis algorithm that is especially tailored to the GUI glue code setting. The environment assumptions and system guarantees for the GUI glue code implementation are represented as universal very-weak Büchi automata, which induce a natural order over the positions in the game into which the obligations of the players are encoded. This is useful in combination with an execution semantics in which GUI glue code can react to every input event with a sequence of actions. This is not only the right model for GUI glue code, but also leads to a drastic reduction of the size of the game graph when adding only sequences of actions that are optimal with respect to the natural order over the successor positions. In this way, we obtain several orders of magnitude of synthesis speed improvement in contrast to other state-of-the-art reactive synthesis approaches that target general reactive systems.While providing a big efficiency improvement overall, the new synthesis process shifts the difficulty of the problem from solving the game to building a relatively small game. This is an unprecedented situation in reactive synthesis, where the most pressing problem is normally that the games built in this approach are too huge to handle for any available game solving method. In the second phase of this project, we will exploit the small size of the games built in our approach. We will research a method to infer the sensible action sequences for the system from the specification before the actual synthesis process, which will further speed up this process. This efficiency improvement is accompanied by a novel approach to infer invariants from computed explicit-state strategies that capture the long-term strategic choices of the synthesized implementations and show the GUI engineer which trade-offs between GUI element availability and long-term planning for specification satisfaction had to be made.Both algorithmic improvements pave the way to bringing the approach into the industrial software development practice by allowing to tackle large-scale GUI specifications and providing confidence in the synthesized GUI glue code.

• DFG Programme: Research Grants