Model checking user interfaces

Abstract

Complex user interfaces are prone to bugs which might be difficult to find by means of testing. To ensure correctness, one would have to develop and run test cases for all possible execution paths within a system. Model checking provides a way to automatically check whether a property holds within all possible execution paths of the system. The model checking process involves modelling the system to be verified using the input language of the model checker being used, formally specifying the properties which are to be verified, then input both formalisms to the model checker. The model checker will then automatically determine whether the properties hold or not, and if not, possibly provide a counterexample to show a countertrace to the property. The problem with model checking is that the process is exponential, however this does not make it unusable. Depending on the nature of the properties we want to verify, we may abstract the system to obtain a relevantly small state space which is model checkable. In this work we look at how we can model check a number of properties which are relevant to the user interface of a system by abstracting a model of the user interface. Since user interfaces are classified as reactive systems, a temporal logic is used to describe the properties we want to verify. Temporal logic is ideal since models contain several states and it has a dynamic notion of truth, allowing a formula to be true in some states and false in others. Thus, the static notion of truth is replaced by a dynamic one, in which a formula may change its truth value as the system evolves from state to state. The aim of this project is to help the automation of model checking a system's user interface and show how a system's user interface may be model checked. The first task is to provide a means of automatically abstracting the user interface of a system. Secondly, a mechanism is to be built to translate the abstracted model into the model checker's input format. Thirdly, the properties we want to verify are to be formalized. Finally, both formalisms are used as input to the model checker. If the model checker provides a counterexample, we shall use this to obtain a visualization of the counterexample to help the system developer trace the possible bug. This project was successful at demonstrating how user interfaces may be automatically abstracted to be model checked for correctness. A case study was carried out to show how the project can be used where a number of properties were verified and a demonstration of how counterexamples are visualized is found in the report.