Automated framework for formal operator task analysis

Aberrant behavior of human operators in safety critical systems can lead to severe or even fatal consequences. Human operators are unique in their decision making capability, judgment and nondeterminism. There is a need for a generalized framework that can allow capturing, modeling and analyzing the interactions between computer systems and human operators where the operators are allowed to deviate from their prescribed behaviors for executing a task. This will provide a formal understanding of the robustness of a computer system against possible aberrant behaviors by its human operators. We provide a framework for (i) modeling the human operators and the computer systems; (ii) formulating tolerable human operator action variations(protection envelope); (iii) determining whether the computer system can maintain its guarantees if the human operators operate within their protection envelopes; and finally, (iv) determining robustness of the computer system under weakening of the protection envelopes. We present Tutela, a tool that assists in accomplishing the first and second step, automates the third step and modestly assists in accomplishing the fourth step.