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

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

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.