A Formal Basis for Modelling Process and Task Management Aspects of User Interface Design

This paper presents a method for formally specifying and reasoning about process models for interactive systems. The method addresses two important aspects of user interface design: controlled but flexible access to functionality; and provision of useful task management information, such as indicating what progress has been made towards achieving goals and what remains to be done. The method is well suited to “data intensive” applications in which the system is being used to manage complex “configurations” of interconnected objects, and for which task goals can be expressed in terms of properties of the underlying configuration of objects. The method includes proof obligations to check the accuracy of the task management information. The paper illustrates the method on a Theory Manager, which manages a store of theorems and proofs; the store has complex consistency and completeness requirements.