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: Melvin E. Conway, Design of a separable transition-diagram compiler, Communications of the ACM, v.6 n.7, p.396-408, July 1963 [doi>10.1145/366663.366704]
• 2: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 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: 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: Paul R. Hanau , David R. Lenorovitz, Prototyping and simulation tools for user/computer dialogue design, ACM SIGGRAPH Computer Graphics, v.14 n.3, p.271-278, July 1980
• 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: 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: C. Heitmeyer , C. Landwehr , M. Cornwell, The use of quick prototypes in the secure military message systems project, ACM SIGSOFT Software Engineering Notes, v.7 n.5, p.85-87, December 1982
• 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: Jacob, R.J.K. Survey and examples of specification techniques for user interfaces. NRL Report, Naval Research Laboratory, Washington, D.C., (To appear).
• 11: Johnson, S.C. Language development tools on the Unix system. IEEE Computer 13, 8 (Aug. 1980), 16-21.
• 12: MUMPS Development Committee. MUMPS language standard. American National Standards Institute, New York, 1977.
• 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: David L. Parnas, On the use of transition diagrams in the design of a user interface for an interactive computer system, Proceedings of the 1969 24th national conference, p.379-385, August 26-28, 1969 [doi>10.1145/800195.805945]
• 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: 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: Andrew Jay Singer, Formal methods and human factors in the design of interactive languages, 1979
• 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: W. A. Woods, Transition network grammars for natural language analysis, Communications of the ACM, v.13 n.10, p.591-606, Oct. 1970 [doi>10.1145/355598.362773]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: User interfaces

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

  H. Information Systems
  H.1 MODELS AND PRINCIPLES
      H.1.2 User/Machine Systems
          Subjects: Human factors

General Terms:
Design, Human Factors, Languages

Keywords:
BNF, interactive languages, specification languages, state transition diagrams, user agent