Programs with Graphical User Interfaces (GUIs) are hard to develop. Rather than arranging the program instructions in the order in which they are executed, for GUI code, the
programmer needs to write event handlers that describe the program's response to certain events. Depending on the completion time of the program's computation threads and
the user's behavior, event handlers can be executed in hard to predict multitude and order. It is easy for the developer to forget possible sequences of events, which makes
the development of GUI code error-prone. While automated frameworks for testing user interface code are available, they do not guarantee that no important case is missed and
they do not improve the efficiency of the actual development process.
In this project, we will research algorithms for reactive synthesis of graphical user interface code. Synthesis algorithms automatically compute finite-state implementations from their specifications. We target the GUI glue code in this project, which connects the main functionality of the program with the user interface. GUI glue code responds to events such as clicks of buttons and thread completion by spawning new threads and changing the state of the GUI. Traditional algorithms for reactive synthesis are not well-suited for synthesizing GUI glue code as they do not scale well enough to deal with the large size of the needed specifications. However, they also do not take advantage of the special properties of the problem. In particular, specifications for GUI glue code have simple components and can be represented as universal very-weak automata (UVWs). When building synthesis games from such specifications, whose winning strategies are the implementations to be synthesized, the simple structure of UVWs enables the use of a variety of symbolic reasoning techniques. Apart from the application of anti-chains for solving the games, we will study the use of monotone boolean learning as main computational engine for game solving in this project. We will construct synthesis algorithms that make use of the properties of the application domain and that deliver implementations of high quality, i.e., that are small and only deactivate GUI elements when needed for soundness.
We will focus on the algorithmic questions in this project, namely which symbolic reasoning engine offers the needed scalability for practical GUI glue code synthesis, and how we can ensure high quality of the generated implementations. All tools to be developed will be on the academic prototype level and will be used to prove the needed scalability of the approach for practical applications. This proof allows to bring the topic closer to the practice of software development after the end of the project.
This project is funded by the German Research Foundation (DFG).