Analyzing Mode Confusion via Model Checking.

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1999
Accession Number
ADA364801

Entities

People

  • Gerald Luettgen
  • Victor Carreno

Organizations

  • National Aeronautics and Space Administration

Tags

Communities of Interest

  • Engineered Resilient Systems
  • Space

DTIC Thesaurus Topics

  • Automata
  • Automation
  • Case Studies
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Control Systems
  • Electronic Mail
  • Engineering
  • Flight Decks
  • Graphical User Interface
  • Guidance
  • Language
  • Machines
  • Neurobehavioral Manifestations
  • Programming Languages

Readers

  • Educational Psychology
  • Mathematical Modeling and Probability Theory.
  • Wave Propagation and Nonlinear Chaotic Dynamics.