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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Analyzing Mode Confusion via Model Checking


    Beteiligte:

    Erscheinungsdatum :

    01.05.1999


    Medientyp :

    Sonstige


    Format :

    Keine Angabe


    Sprache :

    Englisch




    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