Speaker
Mr
B. Wortelen
(OFFIS)
Description
Activity: TRP
ESA TOs: Ms. Maite Trujillo - Independent Safety Office & Mr. Yuri Yushtein - Software Systems Division
Considering human factor issues during system engineering supports the development of systems which compensate limitations and support strengths of human behaviour characteristics. The objective of the VASCO study is the development and validation of a methodology for formal verification of human-automation interaction in safety critical environments based on models of the overall human-automation system. The developed Formal Verification Methodology approaches human-automation interaction from a holistic cooperative system perspective where the object of design is a system of human agents (operators) and machine agents (automated systems) jointly performing a series of tasks (e.g., acquiring data, computing trajectories) aiming at satisfying higher level global tasks (e.g., controlling a spacecraft).
This talk will present: 1) a database of analysis questions that address relevant aspects of human-automation interaction together with a catalogue of formal methods to approach these analysis questions, 2) the Formal Verification Methodology that is used to perform the verification of analysis questions, and 3) experiences and results of a case study used to validate the Formal Verification Methodology. As case study the air flow subsystem of the ISS Columbus module was chosen.
The case study demonstrates that using formal verification techniques for the analysis of human-automation interaction is feasible. However, it revealed that a high modelling effort and utilization of standards for modelling is a prerequisite for an efficient integration of the Formal Verification Methodology in system design processes.
