SHF:Small:Proving User Interface Testing Programs Correct

The Graphical User Interface (GUI) that is ubiquitous in today's computing world consumes about 60% of the software development cost of a GUI APplication (GAP) and as much as 45-60% of its code. Ensuring the quality of GAPs is extremely important for a society that is increasingly reliant on GAPs to manage all aspects of users' lives. Currently, although there are hundreds of GUI testing approaches, algorithms and tools, the field is deeply fragmented and lacks common abstractions, and it is very difficult to integrate different UI testing approaches so as to create powerful solutions to the problems of Reusing and Repairing UI test suites while also Reducing their execution time and resource demands (R3).

The goal of this proposal is therefore to create a novel theoretical foundation to connect these R3 problems with the problem of proving the behavior of complex Programs for User Interface Testing (PUITs), especially when the structure and the functionality of a GAP is constantly changed during its evolution and maintenance.

A connecting thread in the research thrusts of this proposal is to abstract PUITs as functional reactive systems using Eilenberg's X-Machine, which is a generalization of a Finite State Automaton (FSA) in which state transitions are associated with functions which operate on the FSA's data. Test engineers are to create PUITs using a formal functional language in a proof management system called Coq.

The research team is expanding the Razet theorem package for Coq that contains a generic proof for Eilenberg's X-Machine to apply to arbitrary GAPs using the types generated from the GAP FSA. Since the physical structure of the GAP is abstracted away from its PUITs, it is being shown that their reuse will be enabled on different functionally related GAPs.

The resulting verified executable PUITs can be generated automatically in a target language using the Coq's generation facilities. The benefits of the proposed research direction are much bigger than the sum of its constituent parts since a new property of type-directed verification emerges that enables automated reasoning of PUITs, which are created using the semantics of the data in the UI objects, and that enable test engineers not only to prove PUITs correct but also to address R3 problems from a unified perspective.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.