Speaker
Mr
R. van Paassen
(TU Delft)
Description
Activity: GSP
ESA TOs: Ms. Maite Trujillo - Independent Safety Office & Mr. Yuri Yushtein - Software Systems Division
HAI (Human Automation Interaction) is often a contributor to failures in complex systems. These failures are frequently caused by system interactions that were not anticipated by designers or analysts. While there are many useful analysis techniques that can be used to address these types of problems, none consider all of the possible interactions that can occur and can thus miss critical system conditions. Formal verification, and in particular model checking, is capable of such exhaustive analyses. In model checking, the behavior of a target system is represented in a formal model. Specification properties, which describe either desirable or undesirable behavior of the system, are constructed for this model. A model checker then proves (formally verifies) whether or not the model adheres to the specification by automatically searching through the model’s entire state space. One approach for using formal method to evaluate HAI focuses on including models of human behavior in the formal system model so that the impact of human behavior on system safety can be evaluated with a model checker. The presented project extended this method and evaluated it by using it to analyze the HAI of two realistic, aerospace test cases.
EOFM (Enhanced Operator Function Model) is an XML-based language for modeling human task analytic behavior that can be evaluated with formal methods. An automated translator is available that is capable of representing the human behavior captured in an EOFM in the input language of a model checker (SAL; Symbolic Analysis Library) so that it can be included in a larger formal system model. The EOFM to SAL translator also supports two different types of erroneous behavior generation that enables analysts to optionally include human errors in an EOFM’s formal model representation. Collectively, these features allow analysts to use model checking to evaluate whether or not a system satisfies safety properties with both normative and potentially unanticipated erroneous human behavior. Previous work on EOFM required analysts to manually formulate the specification properties they intended to check. Such a practice can be prone to analyst error and oversight. Thus, in the work developed for this project, EOFM was extended to automatically generate specification properties capable of evaluating a system’s HAI, giving analyst a means of potentially finding unanticipated HAI problems.
The EOFM-supported methodology was evaluated in two test cases, a satellite ground station control system and an unmanned air vehicle (UAV) ground control system. Results from the evaluation show that the methodology allows normative representations of human-interactive systems to be modeled and formally verified against manually created safety specifications. The method also enables the generation of specification properties from task models, which are capable of detecting potentially unanticipated problematic HAI conditions. Finally, it supports the inclusion of generated erroneous behaviors that can be used to evaluate the robustness of the system’s HAI and the system’s safety.
