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

本研究的目的是开发网络物理系统人机界面的形式化验证工具。该方法通过数学构建的“错误模型”，针对操作员在交互任务中犯下的常见错误类型，将有关人类行为的现实假设纳入验证过程。详尽的验证技术用于暴露可能导致系统范围故障的人为错误组合。使用涉及医疗设备接口的案例研究来评估这些技术。验证人机界面的问题需要将严格的形式化验证技术与以人为中心的经验方法相结合的新方法来进行用户界面评估。该研究解决了将经验用户研究数据整合到描述常见操作员错误类型的正式游戏模型中的挑战。使用这些模型来检测用户界面设计中的细微缺陷也是一个挑战。众所周知，设计不良的界面会导致操作员出现有害的错误，这仍然是各种安全关键型网络物理系统失败的主要原因。该项目将在设计过程的早期通过检测可能的缺陷来自动化用户界面验证。开源验证工具将免费提供给整个社区。正在进行的研究将整合到一套以“人机界面安全”为主题的研究生水平的计算机科学课程中。该项目的成果也将被整合到正在进行的eCSite GK12项目的教育材料中，目的是提高高中生对用户界面设计问题的认识。

The objective of this research is to develop formal verification toolsfor human-computer interfaces to cyber-physical systems. The approachis incorporating realistic assumptions about the behavior of humans intothe verification process through mathematically constructed "mistakemodels" for common types of mistakes committed by the operator duringan interactive task. Exhaustive verification techniques are used toexpose combinations of human mistakes that can lead to system-widefailures. The techniques are evaluated using case studies involvingmedical device interfaces.The problem of verifying human-machine interfaces requires newapproaches that combine rigorous formal verification techniques withthe empirical human-centered approach to user-interface evaluation.The research addresses challenges of integrating empirical user-studydata into formal game-based models that describe common types of operator mistakes. Using these models to detect subtleflaws in user-interface design is also a challenge.It is well-known that a poorly designed interface will enable harmfuloperator errors, which remain a major cause of failures in a widevariety of safety-critical cyber-physical systems. This project willautomate user-interface verification by detecting likely defects,early in the design process. Open source verification tools will bemade freely available to the community at large. The ongoing researchwill be integrated into a set of graduate-level computer sciencecourses focused on the theme of "Safety in Human Computer Interfaces".Results from the project will also be integrated into educationalmaterials for the ongoing eCSite GK12 project with the goal ofpromoting awareness of user-interface design issues amongst highschool students.