TC: Small: Formalizing Operator Task Analysis

计算机系统通常与人类操作员相结合，人类操作员为计算机编程及其传感器和执行器添加手、眼和判断。 操作员可以被视为编程平台，手册，培训和系统反馈提供编程。 然而，与计算机相比，操作员具有独特的平台特性，特别是包括可能会犯许多不同的错误。因此，依赖于操作员的系统需要一个保护信封，代表一个工程化的系统行为集合，以防止重要类型的操作员错误导致损失。 有一个精心选择的保护信封是至关重要的鲁棒性的系统，依赖于人类操作员。该项目基于为并发进程的形式化分析而创建的模型、语言和技术来形式化操作员任务分析，并使用这种形式化来指定和自动证明依赖于人类操作员在指定环境中安全执行的系统的保护任务的属性。 该项目使用并发的游戏结构提供了一个技术基础，推理aboutprotection envelopes指定使用交替时间时序logic.Progress验证与机场筛选和兽医标记协议的案例研究。 对这类贡献的兴趣将超越喷气式飞机飞行员和核电站运营商等专业领域，扩展到以下角色：电子商务交易或自动零售结账的客户，新型计算机控制汽车的驾驶员，智能仓库，工厂车间和办公大楼的管理者，以及紧急情况下的第一响应者。

Computer systems are commonly coupled with human operators who addhands, eyes, and judgment to the computer programming and its sensorsand actuators. The operators can be viewed as programming platformsin their own right, where manuals, training, and system feedbackprovide the programming. However, operators have unique platformcharacteristics compared to computers, including, in particular, thelikelihood of making numerous and diverse errors. Hence systems thatrely on operators require a protection envelope representing anengineered collection of system behaviors that prevent important typesof operator errors from leading to losses. Having a well chosenprotection envelope is crucial to the robustness of a system thatrelies on human operators. This project formalizes operator taskanalysis based on models, languages, and techniques created for theformal analysis of concurrent processes and use this formalization tospecify and automatically prove properties of the protection envelopesof systems that rely on human operators for their safe and secureexecution in specified environments. The project uses concurrent gamestructures to provide a technical foundation for reasoning aboutprotection envelopes specified using alternating-time temporal logic.Progress is validated with case studies for airport screening andveterinary tagging protocols. Interest in this type of contributionwill extend beyond specialized areas like jet pilots and nuclear plantoperators to roles like: customers in ecommerce transactions orautomated retail checkouts, drivers in automobiles with new types ofcomputer control, managers of smart warehouses, factory floors, andoffice buildings, and first responders in emergencies.