Text size
  • Small
  • Medium
  • Large
Contrast
  • 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

    AUTHORS

    R.J. Butterworth & D.J. Cooke

    ABSTRACT

    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.

    PAPER FORMATS

    PDF filePDF Version of this Paper (140kb)