A formal methods approach to semiotic engineering. Issue 115 (July 2018)

• Record Type: Journal Article
• Authors: Abbate, A.J.; Bass, E.J.
• Is Part Of: International journal of human-computer studies. Issue 115(2018)
• Page Start: 20
• Page End: 39
• Publication Date: 2018-07
• Subjects: Signifiers -- Formal methods -- Semiotic engineering -- Usability -- Human-computer interaction; Human-machine systems -- Periodicals; Systems engineering -- Periodicals; Human engineering -- Periodicals; Human engineering; Human-machine systems; Systems engineering; Periodicals; Electronic journals; 004.019
• DOI: 10.1016/j.ijhcs.2018.02.001
• Languages: English
• ISSNs: 1071-5819

Abstract

Highlights: 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. Abstract: 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.