A formal methods approach to semiotic engineering

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.