Typically formal notations for interactive systems previously presented in the literature ( e.g . [2, 6, 18]) synthesize two or more languages. We contend that it would be preferable if one were able to use a single soundly based specification language which is expressive enough to capture HCI issues. Taking a lead from Lamport’s Temporal Logic ofActions, (TLA),  we outline a language for expressing models of systems based on temporal logic, and make clear the design process we intend this language to be a part of. We discuss two equivalent specification styles using this language; firstly describing the functionality of the system and secondly describing the interactions of the system. We contend that the second is more ‘HCI-centric’ than the first. We discuss other issues raised by the use of the language and set down an agenda for future work.
Author and article information
Computer Studies Department, Loughborough University
Loughborough, Leicestershire, England.