Computer systems are commonly coupled with human operators who add hands, eyes, and judgment to the computer programming and its sensors and actuators. The operators can be viewed as programming platforms in their own right, where manuals, training, and system feedback provide the programming. However, operators have unique platform characteristics compared to computers, including, in particular, the likelihood of making numerous and diverse errors. Hence systems that rely on operators require a protection envelope representing an engineered collection of system behaviors that prevent important types of operator errors from leading to losses. Having a well chosen protection envelope is crucial to the robustness of a system that relies on human operators. This project formalizes operator task analysis based on models, languages, and techniques created for the formal analysis of concurrent processes and use this formalization to specify and automatically prove properties of the protection envelopes of systems that rely on human operators for their safe and secure execution in specified environments. The project uses concurrent game structures to provide a technical foundation for reasoning about protection envelopes specified using alternating-time temporal logic. Progress is validated with case studies for airport screening and veterinary tagging protocols. Interest in this type of contribution will extend beyond specialized areas like jet pilots and nuclear plant operators to roles like: customers in ecommerce transactions or automated retail checkouts, drivers in automobiles with new types of computer control, managers of smart warehouses, factory floors, and office buildings, and first responders in emergencies.
TC: Small: Formalizing Operator Task Analysis