FMitF: Collaborative Research: Track I: Preventing Human Errors in Cyber-human Systems with Formal Approaches to Human Reliability Rating and Model Repair

FMITF：协作研究：第一轨道：通过人类可靠性评级和模型修复的正式方法防止网络人类系统中的人为错误

• 批准号: 1918140
• 负责人: Eunsuk Kang
• 金额: $ 37.5万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-08-15 至 2023-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1918140&HistoricalAwards=false
• 关键词: FMitF; Collaborative; Research; Track; Preventing

Human error is a major factor in failures across safety-critical domains. Such failures are very complex, with human errors often arising as a result of unexpected interactions between system automation and human behavior. Thus, researchers have investigated how formal methods tools and techniques, which have been developed to mathematically prove properties about complex computer systems, can be adapted to human-automation interaction (HAI) problems. These techniques are powerful and capable of discovering unexpected, critical human errors and system failures. However, existing techniques do not provide a means for fixing discovered human errors. Further, interface changes both introduce new unforeseen errors and risk negative transfer effects, where changes that conflict with previously learned behaviors can also cause problems. This project will investigate a novel approach to HAI evaluation and repair that will help designers and analysts efficiently eliminate many kinds of potential interaction errors while minimizing the risk of introducing additional human errors. The developed methods will be validated in design cases of real safety-critical systems including an industrial furnace, nuclear power plant procedures, a radiation therapy machine, and pharmacy medication dispensing processes. The knowledge and tools produced in this research will be made available to researchers and designers and have potential applications to a wide range of many safety-critical systems. This, in turn, will help avoid system disasters, prevent injuries, save lives, and protect critical resources across society.The project is divided into three main thrusts. First, the team will develop a theoretically grounded method for scoring the likelihood that humans will behave erroneously for a given HAI design through a novel synthesis of formal methods, erroneous human behavior models, negative transfer theory, and human reliability analyses. Second, it will introduce a new theory of formal model repair in interactive systems that will underlie the development of methods for removing problematic HAI errors by adapting both human-machine interfaces and the workflow of the associated tasks. Third, the scoring and model repair methods will be combined to allow automated model repair to find design interventions that will reduce the likelihood of changes causing problematic human errors, using a database of common error patterns and solutions to be developed through the project. Across all three of these thrusts, the team will use human subject experiments, testing, and formal proofs to validate that the advances achieve their hypothesized capabilities. The work will lead to improved methods for evaluating human reliability aspects of interfaces, widen the application of formal methods to new contexts, and provide resources for researchers, designers, and engineers to improve the reliability of cyber-human systems.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

人为错误是安全关键领域故障的主要因素。 这种故障非常复杂，人为错误通常是由于系统自动化和人类行为之间的意外交互而产生的。 因此，研究人员已经研究了如何正式的方法工具和技术，这已经发展到数学证明复杂的计算机系统的属性，可以适应人类自动化交互（HAI）的问题。这些技术功能强大，能够发现意外的关键人为错误和系统故障。然而，现有技术没有提供用于修复所发现的人为错误的手段。此外，界面的变化既会引入新的不可预见的错误，也会带来负面的迁移效应，而与之前学习的行为相冲突的变化也会导致问题。 该项目将研究一种新的HAI评估和修复方法，帮助设计师和分析师有效地消除多种潜在的交互错误，同时最大限度地减少引入额外人为错误的风险。所开发的方法将在真实的安全关键系统的设计案例中进行验证，这些系统包括工业炉、核电站程序、放射治疗机和药房药物分配过程。在这项研究中产生的知识和工具将提供给研究人员和设计人员，并有潜在的应用范围广泛的许多安全关键系统。这反过来将有助于避免系统灾难，防止伤害，拯救生命，并保护整个社会的关键资源。 首先，该团队将开发一种理论基础的方法，通过正式方法，错误的人类行为模型，负迁移理论和人的可靠性分析的新合成，对人类在给定的HAI设计中错误行为的可能性进行评分。其次，它将引入交互系统中形式模型修复的新理论，该理论将成为通过调整人机界面和相关任务工作流程来消除有问题的HAI错误的方法开发的基础。 第三，评分和模型修复方法将结合起来，使自动模型修复找到设计干预措施，将减少可能造成人为错误的变化，使用一个数据库的常见错误模式和解决方案将通过该项目开发。在所有这三个方面，该团队将使用人类受试者实验，测试和正式的证据来验证这些进步实现了他们假设的能力。 这项工作将导致改进的方法来评估人的可靠性方面的接口，扩大正式的方法，以新的上下文的应用，并提供资源，为研究人员，设计师和工程师，以提高可靠性的网络人类systems.This奖项反映了NSF的法定使命，并已被认为是值得的支持，通过评估使用基金会的智力价值和更广泛的影响审查标准。

项目成果

Robustification of Behavioral Designs against Environmental Deviations

针对环境偏差的行为设计的鲁棒性

• DOI: 10.1109/icse48619.2023.00046
• 发表时间: 2023
• 期刊: 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE
• 作者: Zhang, Changjian;Saluja, Tarang;Meira-Góes, Rômulo;Bolton, Matthew;Garlan, David;Kang, Eunsuk
• 通讯作者: Kang, Eunsuk

A formal method for including the probability of erroneous human task behavior in system analyses

将错误人类任务行为的概率纳入系统分析的正式方法

• DOI: 10.1016/j.ress.2021.107764
• 发表时间: 2021
• 期刊: Reliability Engineering & System Safety
• 影响因子: 8.1
• 作者: Bolton, Matthew L.;Zheng, Xi;Kang, Eunsuk
• 通讯作者: Kang, Eunsuk

Synthesis of Assurance Cases for Software Certification

软件认证保证案例综合

• DOI: 10.1145/3377816.3381728
• 发表时间: 2020
• 期刊: Proceedings of the International Conference on Software Engineering
• 作者: Bagheri, Hamid;Kang, Eunsuk;Mansoor, Niloofar
• 通讯作者: Mansoor, Niloofar

AlloyMax: bringing maximum satisfaction to relational specifications

• DOI: 10.1145/3468264.3468587
• 发表时间: 2021-08
• 期刊: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
• 作者: Changjian Zhang;Ryan Wagner;Pedro Orvalho;D. Garlan;Vasco M. Manquinho;R. Martins;Eunsuk Kang