Logo image
Back
A formal methods approach to semiotic engineering
Journal article   Peer reviewed

A formal methods approach to semiotic engineering

A.J. Abbate and E.J. Bass
International journal of human-computer studies, v 115, pp 20-39
Jul 2018
DOI: https://doi.org/10.1016/j.ijhcs.2018.02.001

Abstract

Formal methods Human-computer interaction Semiotic engineering Signifiers Usability
•This work introduces a formal methods approach to semiotic engineering.•Methods support the modeling of human–system interface signifiers.•Measures reason about effective and efficient designer-to-user communication.•Potential designer-to-user communication problems are identified in a medical device case study. This work introduces a formal methods approach to semiotic engineering: Browser-Integrated Guidance for Specifying Interface Signifiers (BIGSIS). Drawing from the semiotic engineering and formal methods literature, BIGSIS facilitates logical reasoning about human-system interface signifiers with respect to measures of effective and efficient designer-to-user communication. Signifiers that communicate correct functions or meanings are effective, and signifiers that convey nonconflicting functions or meanings are efficient. The BIGSIS approach incorporates a five-step process, an XML syntax, a Z notation formalism, an XML-to-Symbolic-Analysis-Laboratory (SAL) translator, and three signifier specifications: internal consistency, inter-channel consistency, and completeness. These elements of the approach support two analyses: BIGSIS-XML and model checking. The BIGSIS-XML analysis addresses one interface component, one sensory channel (visual, audio, or haptic), and one target-system configuration at a time. Using SAL, the model checking analysis considers all interface components including documentation, sensory channels, and a broad range of target-system configurations. We demonstrate an application of BIGSIS with a medical device case study. The analysis considers four components on the system’s controller, three sensory channels, and signified information from U.S. cultural context and explanations within an accompanying patient handbook. The BIGSIS-XML analysis aids in identifying 12 potential designer-to-user communication problems: ten involving effectiveness and two involving efficiency. The model checking analysis aids in identifying six potential designer-to-user communication problems: four involving effectiveness and two involving efficiency. Case study results indicate that BIGSIS shows promise for identifying potential instances of ineffective and inefficient designer-to-user communication in the design of a complex, safety-critical system interface.

Metrics

4 Record Views
7 citations in Scopus

Details

Logo image