TC: Small: Formalizing Operator Task Analysis

点击翻译按钮获取中文摘要

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.