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.
Human operators are an integral part of Cyber-Physical Systems. Modeling the interactions of these operators with the system, and analyzing the effects of the faults in these interactions is an important, heretofore unmet challenge. This challenge is faced everyday by operators of critical devices such as drug and insulin infusion pumps that control the delivery of critical drugs to patients suffering from chronic illness such as type-1 diabetes. This project focused on modeling and analyzing models of human users of CPS, with a special emphasis on infusion pumps. We were able to successfully create comprehensive models of human operators of drug and insulin infusion pumps and verify important properties of these models. Our modeling approaches allowed for various human and environment induced faults; mapping a combination of such faults to a final outcome in terms of property violations. At the other end, our work examined low level user interfaces that are prone to issues such as mode confusion and interface faults that can promote harmful user errors. At this level, our work combined computer vision techniques with grammatical inference to build internal models of interfaces from external interactions with the interface. We extended this work to directly observe issues such as mode confusion and other user-specified property violations in interfaces. Finally, our work has been applied extensively to drug and insulin infusion pumps. For these devices, we modeled the overall closed loop that includes the device as well as the human operator models, allowing for device as well as human faults. Our work resulted in numerous publications at prestigious venues. Further dissemination was carried out through talks at various seminars and colloquia. The models and code developed are available through our website: http://systems.cs.colorado.edu/research/cyberphysical/infusion-pump-analysis/
