Using formal specifications in the design of a human-computer interface

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.

References

1. 1 Conway, M.E. Design of a separable transition-diagram compiler. Comm. ACM S, 7 (July 1963), 396-408.
2. 2 Dijkstra, E.W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976, pp. 209-217.
3. 3 Embley, D.W. Empirical and formal language design applied to a unified control construct for interactive computing. Int. I. Man- Machine Studies 10, 2 (March 1978), 197-218.
4. 4 Foley, J.D. and Wallace, V.L. The art of graphic man-machine conversation. Proceedings of the IEEE 62, 4 (April 1974), 462-471.
5. 5 Hanau, P.R. and Lenorovitz, D.R. Prototyping and simulation tools for user/computer dialogue design. Computer Graphics 14, 3 (July 1980), 271-278.
6. 6 Heitmeyer, C.L. and Wilson, S.H. Military message systems: Current status and future directions. IEEE Transactions on Communications COM-2S, 9 (Sept. 1980), 1645-1854.
7. 7 Heitmeyer, C.L. An intermediate command language (ICL) for the family of military message systems. Technical Memorandum 7590- 450:CH:ch, Naval Research Laboratory, Washington, D.C., 13 Nov. 1981.
8. 8 Heitmeyer, C.L., Landwehr, C.E., and Cornwell, M.R. The use of quick prototypes in the military message system project ACM SIGSOFT. Software Engineering Notes 7, 5 (Dec. 1982).
9. 9 Hueras, J.F. A forrhalization of syntax diagrams as k-deterministic language recognizers. M.S. thesis, Computer Science Dept., Univ. California, Irvine, 1978.
10. 10 Jacob, R.J.K. Survey and examples of specification techniques for user interfaces. NRL Report, Naval Research Laboratory, Washington, D.C., (To appear).
11. 11 Johnson, S.C. Language development tools on the Unix system. IEEE Computer 13, 8 (Aug. 1980), 16-21.
12. 12 MUMPS Development Committee. MUMPS language standard. American National Standards Institute, New York, 1977.
13. 13 Moran, T.P. The command language grammar: A representation for the user interface of interactive computer systems. Int. 1. Man-Machine Studies 15, 1 (July 1981), 3-50.
14. 14 Parnas, D.L. On the use of transition diagrams in the design of a user interface for an interactive computer system. Proc. 24th Nat'l ACM Conference (1989), 379-385.
15. 15 Reisner, P. Formal grammar and human factors design of an interactive graphics system. IEEE Trans. Software Eng. SE-7, 2 (March 1981), 229-240.
16. 16 Shneiderman, B. Multi-party grammars and related features for defining interactive systems. IEEE Trans. Systems, Man, and Cybernetics SMC-12, 2 (March 1981), 148-154.
17. 17 Singer, A. Formal methods and human factors in the design of interactive languages. Ph.D. dissertation, Computer and Information Science Dept., Univ. Massachusetts, 1979.
18. 18 Wilson, S.H,, Kallander, J.W., Thomas, N.M, III, Klitzkie, L.C., and Bunch, J.R, Jr. MME quick look report. Memorandum Report 3992, Naval Research Laboratory, Washington, D.C., 1979.
19. 19 Woods, W.A. Transition network grammars for natural language analysis. Comm. ACM 13, 10 (Oct. 1970), 591-606.

Index Terms

• Human-centered computing

  • Human computer interaction (HCI)

• Software and its engineering

  • Software notations and tools

    • Development frameworks and environments

      • Integrated and visual development environments

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program specifications