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.
The use of formal methods to characterize human parts of a complexsystem that inlcudes computers is a growing area of interest that hasbeen well-informed by our studies. This effort has been particularlyaided by our case studies and these have motivated our mathematicaltheory whcih is able to calculate the robustness of protectionenvelopes under human deviation from their specified tasks. Our formalsemantics of the human task specification language Enhanced OperatorFunction Model with Communication (EOFMC) showed how to incorporatespecifications of human tasks into models of complete systems, and howto provide modular reasoning results for systems depending upon humanprotection envelopes. Based on this work we have introduced prototypetools. Tutela is a tool developed to assist modeling human-computersystems as CGS, giving expected properties, testing the correctness ofcomponents assuming complementary components satisfy theirspecifications, and testing specifications (protection envelopes) fortheir robustness under common perturbations of human action. We havedeveloped a prototype model checker for Rely-Guarantee Temporal Logic.This logic allows us to decompose specifications into properties beingrelied upon (protection envelopes of other components) and propertiesguaranteed. We have developed a prototype for transforming theextensive trace output from simulators to models suitable for modelchecking. Our work on the mathematical models and the tools has beenwritten up, accepted for publication and presented at a range ofresearch conferences. Work from this project has been applied to the area of avionics, whereit has been used to help model and analyze the pilot-automationinteraction. In the NextGenAA project of NASA, there has been repeatedneed to specify and analize operator - system interactions. Inparticular, the concept of protection envelope (core to this project)has been used repeatedly in this project in specifying the complexinteractions of the air-traffic controller, the pilot flying, thepilot monitoring, the flight management system and the autopilot whenthe air-traffic controller issues an advisory and cockpit crewreacts. Example scenarios have been developed both in low level detailfor localized behavior of a heading change, and in the more highlevel, longer term bevaior of the control of a series of aircraft inConituous Descent Arrival into LAX. Rely-Guarantee Temporal Logic(developed under this project) has been used to specify the protectionenvelopes and the dependencies of various systems and operator tasksupon them.
