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

CPS：小型：网络物理系统人机接口的形式分析

• 批准号: 1035845
• 负责人: Sriram Sankaranarayanan
• 金额: $ 45万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-09-15 至 2014-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1035845&HistoricalAwards=false
• 关键词: CPS; Small; Formal; Analysis; Man

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.

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