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.

这项研究的目的是为网络物理系统开发正式的验证工具。该方法通过数学构造的“ mistakeModels”来结合对人类行为的现实假设，以解决操作员在交互式任务期间犯下的常见错误类型。详尽的验证技术用于阐明人类错误的组合，这些错误可能导致系统范围的范围。 使用涉及中介设备界面的案例研究对技术进行了评估。验证人机接口的问题需要新的操作，将严格的正式验证技术与以人类为中心的用户界面评估相结合的方法，以解决经验性的用户studydata将基于Game Game基于游戏的模型整合到普通类型的过程中。使用这些模型来检测用户界面设计中的细微之丝也是一个挑战。众所周知，设计较差的界面将使有害操作器误差造成有害误差，这仍然是造成大量安全关键安全性网络物理系统中失败的主要原因。 该项目将通过在设计过程的早期检测可能的缺陷来验证用户界面验证。开源验证工具将为整个社区免费提供。 正在进行的研究将被整合到一系列以“人类计算机界面安全性”为主题的研究生级计算机科学家。从该项目中进行的分解也将集成到正在进行的Ecsite GK12项目的教育材料中，该项目的目标是在较高级别的学生中涉及使用“用户视觉设计问题”的目标。