Accession Number:

ADA364801

Title:

Analyzing Mode Confusion via Model Checking.

Descriptive Note:

Final rept.,

Corporate Author:

NATIONAL AERONAUTICS AND SPACE ADMINISTRATION HAMPTON VA LANGLEY RESEARCH CENTER

Personal Author(s):

Report Date:

1999-05-01

Pagination or Media Count:

67.0

Abstract:

Mode confusion is one of the most serious problems in aviation safety. Todays 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.

Subject Categories:

  • Military Aircraft Operations
  • Personnel Management and Labor Relations
  • Marine Engineering

Distribution Statement:

APPROVED FOR PUBLIC RELEASE