Joshi, AnjaliMiller, StevenHeimdahl, Mats2020-12-102020-12-10200322nd IEEE Digital Avionics Systems Conference (DASC'2003)} (Awarded Best Paper of Session), Indianapolis, October 2003.https://hdl.handle.net/11299/217336Associated research group: Critical Systems Research GroupAdvancements in digital avionics systems have accounted for much of the improvement in air safety seen over the last few decades. At the same time, the growing complexity of these systems places greater demands on the flight crew and increases the risk of mode confusion, a phenomenon in which pilots become confused about the status of the system and interact with it incorrectly. To fly commercial flights today, pilots must master several complex, dynamically interacting systems, often operating at different levels of automation. These systems typically have many different modes of operation, with different responses to crew actions and the other systems in each mode. Mode confusion occurs when the flight crew believes they are in a mode different than the one they are actually in and consequently make inappropriate requests or responses to the automation. The basis premise behind detecting mode confusion through analysis of system requirements or design specifications is that certain design features or patterns are more likely to cause mode confusion than others. This paper describes the use of automated analysis tools, such as model-checkers and theorem provers, to search for potential sources of mode confusion in a representative specification of the mode logic of a Flight Guidance System. We describe several representative patterns indicative of mode confusion, and show how automated tools can be used to systematically search for such patterns in a requirements or design model.Report