NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Analyzing Mode Confusion via Model CheckingMode 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.
Document ID
19990063915
Acquisition Source
Langley Research Center
Document Type
Other
Authors
Luettgen, Gerald
(Institute for Computer Applications in Science and Engineering Hampton, VA United States)
Carreno, Victor
(NASA Langley Research Center Hampton, VA United States)
Date Acquired
September 6, 2013
Publication Date
May 1, 1999
Subject Category
Air Transportation And Safety
Report/Patent Number
ICASE-RN-9918
NCR-1999-209332
AD-A364801
Funding Number(s)
CONTRACT_GRANT: NAS1-97046
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
Document Inquiry

Available Downloads

There are no available downloads for this record.
No Preview Available