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错误的方法的基础。 第三，将使用评分和模型维修方法，以允许自动化模型维修，以找到设计干预措施，以减少变化的可能性导致有问题的人类错误，并使用通过项目开发的常见错误模式和解决方案的数据库。在所有这三个推力中，团队将使用人类主题实验，测试和正式证明来验证进步是否达到其假设的能力。 这项工作将导致改进的方法来评估界面的人类可靠性方面，扩大正式方法在新环境中的应用，并为研究人员，设计师和工程师提供资源，以提高网络人类系统的可靠性。该奖项反映了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