Experiences from Using Formal Verification Techniques to Analyze Human-Machine Interaction: A Case Study

Using formal verification techniques for the analysis of human-automation interaction can support the design process of safety-critical systems. In recent years several approaches have been developed, which address different problems in the human-automation interaction. In this paper we present our experiences from a one-year study of applying such techniques to analyze the Environmental Control and Life Support System of the Columbus module of the International Space Station.