CPS: Small: Formal Analysis of Man-Machine Interfaces to Cyber-Physical Systems

Abstract: The objective of this research is to develop formal verification tools for human-computer interfaces to cyber-physical systems. The approach is incorporating realistic assumptions about the behavior of humans into the verification process through mathematically constructed "mistake models" for common types of mistakes committed by the operator during an interactive task. Exhaustive verification techniques are used to expose combinations of human mistakes that can lead to system-wide failures. The techniques are evaluated using case studies involving medical device interfaces. The problem of verifying human-machine interfaces requires new approaches that combine rigorous formal verification techniques with the empirical human-centered approach to user-interface evaluation. The research addresses challenges of integrating empirical user-study data into formal game-based models that describe common types of operator mistakes. Using these models to detect subtle flaws in user-interface design is also a challenge. It is well-known that a poorly designed interface will enable harmful operator errors, which remain a major cause of failures in a wide variety of safety-critical cyber-physical systems. This project will automate user-interface verification by detecting likely defects, early in the design process. Open source verification tools will be made freely available to the community at large. The ongoing research will be integrated into a set of graduate-level computer science courses focused on the theme of "Safety in Human Computer Interfaces". Results from the project will also be integrated into educational materials for the ongoing eCSite GK12 project with the goal of promoting awareness of user-interface design issues amongst high school students.