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.

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