Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Using Temporal Logic in the Specification of Reactive and Interactive Systems

    BCS-FACS Workshop on Formal Aspects of the Human Computer Interface

    Sheffield, UK. 10th - 12th September 1996


    R.J. Butterworth & D.J. Cooke


    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 of Actions, (TLA), [14] 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.


    PDF filePDF Version of this Paper (140kb)