A framework for prototyping and mechanically verifying a class of user interfaces

Increasing importance is being attached to the ability of ensuring that graphical user interfaces (GUIs) behave as expected, as they are being used in more applications where safety and security are critical. Prototyping is the preferred approach to creating GUIs because of the need to allow the user to test many of the issues associated with usability. Unfortunately it is often difficult to verify that prototype-based implementations always behave as expected. In this paper we present a framework for prototyping GUI-based applications in which both an implementation (prototype) and a formal model of that implementation are mechanically derived from a description of the application. The model can then be used to support proofs of behavior, while the prototype can be used to test functionality and usability