@inproceedingsJav2014, Author = {Javaux, Denis and Wortelen, Bertram and L├╝dtke, Andreas and Pecheur,Charles and Peldszus, Regina and Sievi, Sonja and Yushtein, Yuri }, Title = {A Methodology for Analyzing Human-Automation Interactions in Flight Operations Using Formal Verification Techniques}, Year = {2014}, Pages = {122-127}, Month = {3}, Publisher = {AAAI Press}, Address = {Palo Alto, CA}, Booktitle = {Formal Verification and Modeling in Human-Machine Systems - Papers from the AAAI Spring Symposium}, Organization = {Association for the Advancement of Artificial Intelligence}, type = {inproceedings}, note = {When designing and developing systems in safety critical or cost intensive environments it is important to identify as much potential risks as possible prior to operating the system. This includes aspects of the interaction between human and automation sy}, Abstract = {When designing and developing systems in safety critical or cost intensive environments it is important to identify as much potential risks as possible prior to operating the system. This includes aspects of the interaction between human and automation systems that are prone to issues. This work-in-progress paper describes a methodology that systematically derives relevant analysis questions for complex human-automation interaction systems. It demonstrates how formal models for all components of the human-automation system can be created. These models are used by model checking algorithms to verify the safety properties associated with the selected analysis questions. While this paper includes no evaluation of the methodology, an ongoing evaluation study is outlined based on the life support system (ECLS) of the European science laboratory Columbus, which is part of the International Space Station. Each step of the formal verification methodology is illustrated with the results obtained so far on the ECLS case study.} @COMMENTBibtex file generated on