Mode confusion is one of the most serious problems in aviation safety. Today's complex digital flight decks make it difficult for pilots to maintain awareness of the actual states, or modes, of the flight deck automation. NASA Langley leads an initiative to explore how formal techniques can be used to discover possible sources of mode confusion. As part of this initiative, a flight guidance system was previously specified as a finite Mealy automaton, and the theorem prover PVS was used to reason about it. The objective of the present paper is to investigate whether state-exploration techniques, especially model checking, are better able to achieve this task than theorem proving and also to compare several verification tools for the specific application. The flight guidance system is modeled and analyzed in Murphi, SMV, and Spin. The tools are compared regarding their system description language, their practicality for analyzing mode confusion, and their capabilities for error tracing and for animating diagnostic information. It turns out that their strengths are complementary.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

    Analyzing Mode Confusion via Model Checking


    Contributors:

    Publication date :

    1999-05-01


    Type of media :

    Miscellaneous


    Type of material :

    No indication


    Language :

    English




    Analyzing Software Specifications for Mode Confusion Potential

    Leveson, Nancy G. / Pinnel, L. Denise / Sandys, Sean David et al. | NTRS | 1998


    Flight Deck Mode Confusion Detection using Intent-based Probabilistic Model Checking

    Suraj Nandiganahalli, Jayaprakash / Lee, Sangjin / Hwang, Inseok | AIAA | 2017


    Flight Deck Mode Confusion Detection Using Intent-based Probabilistic Model Checking (AIAA 2017-0345)

    Nandiganahalli, Jayaprakash Suraj / Lee, Sangjin / Hwang, Inseok | British Library Conference Proceedings | 2017


    An Approach for Eliminating Mode Confusion

    Mumaw, R. J. / Flight Safety Foundation / International Federation of Airworthiness et al. | British Library Conference Proceedings | 2002


    User Interface Validation using Mode Confusion Detection

    Nandiganahalli, J. / Lee, S. / Hwang, I. et al. | British Library Conference Proceedings | 2014