article

Free access

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

Author:

Robert J. K. JacobAuthors Info & Claims

Communications of the ACM, Volume 26, Issue 4

Pages 259 - 264

https://doi.org/10.1145/2163.358093

Published: 01 April 1983 Publication History

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]

Conway, M.E. Design of a separable transition-diagram compiler. Comm. ACM S, 7 (July 1963), 396-408.

Digital Library

[2]

Dijkstra, E.W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976, pp. 209-217.

Digital Library

[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]

Hanau, P.R. and Lenorovitz, D.R. Prototyping and simulation tools for user/computer dialogue design. Computer Graphics 14, 3 (July 1980), 271-278.

Digital Library

[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]

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).

Digital Library

[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.

Digital Library

[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]

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.

Digital Library

[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.

Digital Library

[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]

Singer, A. Formal methods and human factors in the design of interactive languages. Ph.D. dissertation, Computer and Information Science Dept., Univ. Massachusetts, 1979.

Digital Library

[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]

Woods, W.A. Transition network grammars for natural language analysis. Comm. ACM 13, 10 (Oct. 1970), 591-606.

Digital Library

Cited By

Wang HLiu S(2023)A domain knowledge driven approach for user interface software developmentJournal of Computer Science and Technology10.1007/BF029453656:2(145-152)Online publication date: 22-Mar-2023
https://dl.acm.org/doi/10.1007/BF02945365
Benvenuti DFilosa MCatarci TAngelini M(2023)Modeling and Assessing User Interaction in Big Data Visualization SystemsHuman-Computer Interaction – INTERACT 202310.1007/978-3-031-42283-6_5(86-109)Online publication date: 28-Aug-2023
https://dl.acm.org/doi/10.1007/978-3-031-42283-6_5
Flak O(2020)Estimated Influence of Online Management Tools on Team Management Based on the Research with the Use of the System of Organizational TermsIntelligent Systems and Applications10.1007/978-3-030-55187-2_6(56-72)Online publication date: 25-Aug-2020
https://doi.org/10.1007/978-3-030-55187-2_6
Show More Cited By

Index Terms

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

Recommendations

A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Formal test specifications in open systems
ISESS '95: Proceedings of the 2nd IEEE Software Engineering Standards Symposium

The development of formal test specifications for an open system standard is described. The effort is being conducted within the environment provided by the Clemson Automated Testing System (CATS). CATS features the ability to automatically translate ...
Making Changes to Formal Specifications: Requirements and an Example

Formal methods have had little impact on software engineering practice, despite the fact that most software engineering practitioners readily acknowledge the potential benefits to be gained from the mathematical modeling involved. One reason is that ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Communications of the ACM

Communications of the ACM Volume 26, Issue 4

April 1983

68 pages

ISSN:0001-0782

EISSN:1557-7317

DOI:10.1145/2163

Editor:
Peter J. Denning
Purdue Univ., West Lafayette, IN

Issue’s Table of Contents

Copyright © 1983 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1983

Published in CACM Volume 26, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

160
Total Citations
View Citations
1,107
Total Downloads

Downloads (Last 12 months)123
Downloads (Last 6 weeks)14

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wang HLiu S(2023)A domain knowledge driven approach for user interface software developmentJournal of Computer Science and Technology10.1007/BF029453656:2(145-152)Online publication date: 22-Mar-2023
https://dl.acm.org/doi/10.1007/BF02945365
Benvenuti DFilosa MCatarci TAngelini M(2023)Modeling and Assessing User Interaction in Big Data Visualization SystemsHuman-Computer Interaction – INTERACT 202310.1007/978-3-031-42283-6_5(86-109)Online publication date: 28-Aug-2023
https://dl.acm.org/doi/10.1007/978-3-031-42283-6_5
Flak O(2020)Estimated Influence of Online Management Tools on Team Management Based on the Research with the Use of the System of Organizational TermsIntelligent Systems and Applications10.1007/978-3-030-55187-2_6(56-72)Online publication date: 25-Aug-2020
https://doi.org/10.1007/978-3-030-55187-2_6
Jaidka SReeves SBowen J(2019)Formal Modelling of Safety-Critical Interactive Devices Using Coloured Petri NetsFormal Methods. FM 2019 International Workshops10.1007/978-3-030-54994-7_34(465-485)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-54994-7_34
Magnaudet MChatty SConversy SLeriche SPicard CPrun D(2018)Djnn/SmalaProceedings of the ACM on Human-Computer Interaction10.1145/32290942:EICS(1-27)Online publication date: 19-Jun-2018
https://dl.acm.org/doi/10.1145/3229094
Marrella ACatarci TKoskinen ILim YCerratto-Pargman TChow KOdom W(2018)Measuring the Learnability of Interactive Systems Using a Petri Net Based ApproachProceedings of the 2018 Designing Interactive Systems Conference10.1145/3196709.3196744(1309-1319)Online publication date: 8-Jun-2018
https://dl.acm.org/doi/10.1145/3196709.3196744
Isoc D(2017)Expert System for Predictive Diagnosis (2) Implementing, Testing, UsingSoft Computing Applications10.1007/978-3-319-62521-8_4(34-46)Online publication date: 2-Sep-2017
https://doi.org/10.1007/978-3-319-62521-8_4
Mitta D(2016)A Methodology for Quantifying Expert System UsabilityHuman Factors: The Journal of the Human Factors and Ergonomics Society10.1177/00187208910330020733:2(233-245)Online publication date: 23-Nov-2016
https://doi.org/10.1177/001872089103300207
Bauer DEddy J(2016)The Representation of Command Language SyntaxHuman Factors: The Journal of the Human Factors and Ergonomics Society10.1177/00187208860280010128:1(1-10)Online publication date: 23-Nov-2016
https://doi.org/10.1177/001872088602800101
Treacy Solovey EAfergan DPeck EHincks SJacob R(2015)Designing Implicit Interfaces for Physiological ComputingACM Transactions on Computer-Human Interaction10.1145/268792621:6(1-27)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2687926
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents