UO Research Protects Space Vessel
On the night of July 3, 2005 at 10:52 p.m. NASA's Deep Impact became the first space craft to hit a comet. The craft was sent to study the interior of comet Tempel 1, by excavating a crater more than 25 m deep and 100 m in diameter. With $330 million invested, the fault protection system was critical to the mission success. Before the mission could proceed, the fault protection system had to be verified by a team comprised of CIS graduate student Ny Aina Razermera Mamy, Professor Stephen Fickas, and Jet Propulsion Lab researcher Dr. Martin Feather.
The team used a formal verification process that was presented in a paper at the Sixth IEEE International Symposium on High Assurance Systems Engineering. The particular approach used model checking to verify correctness of the hardware and software. Unlike proof-based formal methods, model checking seeks to demonstrate the correctness of the underlying system, without the use of highly abstracted representations. The state machine used in the model checker is exactly the machine generated in code; however, large applications, such as the spacecraft systems, cannot be easily verified because of the complexity of states in which it may find itself. Unless the engineers are skillful, the verfication computations can easily run out of space or time before the process can be completed.
The Fault Protection system monitors the health of the spacecraft's hardware and software, and coordinates and tracks responses to faults that it has detected. Such autonymous software is necessary on space vehicles because of the delays required for human operators on Earth to remotely activate the crafts' systems.