Abstract
Formal specification techniques are valuable in software development because they permit a designer to describe the external behavior of a system precisely without specifying its internal implementation. Although formal specifications have been applied to many areas of software systems, they have not been widely used for specifying user interfaces. In the Military Message System project at the Naval Research Laboratory, the user interfaces as well as the other components of a family of message systems are specified formally, and prototypes are then implemented from the specifications. This paper illustrates the specification of the user interface module for the family of message systems. It then surveys specification techniques that can be applied to human-computer interfaces and divides the techniques into two categories: those based on state transition diagrams and those based on BNF. Examples of both types of specifications are given. Specification notations based on state transition diagrams are preferable to those based on BNF because the former capture the surface structure of the user interface more perspicuously. In either notation, a high-level abstraction for describing the semantics of the user interface is needed, and an application-specific one is used here.
Keywords
Affiliated Institutions
Related Publications
Extending State Transition Diagrams for the Specification of Human–Computer Interaction
User Software Engineering is a methodology for the specification and implementation of interactive information systems. An early step in the methodology is the creation of a for...
Safety analysis of timing properties in real-time systems
The authors formalize the safety analysis of timing properties in real-time systems. The analysis is based on a formal logic, RTL (real-time logic), which is especially suitable...
On the use of transition diagrams in the design of a user interface for an interactive computer system
This paper deals with what might be called the top level design of an interactive computer system. It examines some problems which arise in trying to specify what the user inter...
Tinker 8: Software Tools for Molecular Design
The Tinker software, currently released as version 8, is a modular molecular mechanics and dynamics package written primarily in a standard, easily portable dialect of Fortran 9...
Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models
It is becoming increasingly important that communication protocols be formally specified and verified. This paper describes a particular approach–the state transition model–usin...
Publication Info
- Year
- 1983
- Type
- article
- Volume
- 26
- Issue
- 4
- Pages
- 259-264
- Citations
- 168
- Access
- Closed
External Links
Social Impact
Social media, news, blog, policy document mentions
Citation Metrics
Cite This
Identifiers
- DOI
- 10.1145/2163.358093