NASA Logo, National Aeronautics and Space Administration

Honeywell's DEOS Operation System

This project experiments the Spin model checking system to support automated verification of time partitioning in the Honeywell DEOS real-time scheduling kernel. The goal of the experiment was to investigate whether model checking with minimal abstraction could be used to find a subtle implementation error that was originally discovered and fixed during the standard formal review process. The experiment involved translating a core slice of the DEOS scheduling kernel from C++ into Promela, constructing an abstract "test-driver" enviroment and carefully introducing several abstractions into the system to support verification. Attempted verification of several properties related to time-partitioning led to the rediscovery of the known error in the implementation.

The case study indicated several limitations in existing tools to support model checking of software. The most difficult task in the original DEOS experiment was constructing an adequate enviroment to close the system for verification. The fidelity of the enviroment was of crucial importance for achieving meaningful results during model checking.

Reviewed 2012



NASA Researchers

Honeywell Researchers

  • Eric Engstorm
  • Aaron Larson
  • Nicholas Weininger

Other Info

Publications

First Gov logo
NASA Logo - nasa.gov