Case: Finding Hidden Bugs With T-VEC Solutions

The Problem

Undiscovered code bug is likely cause of Mars Polar Lander crash

Lockheed Martin Space Systems Company Astronautics Operations wanted to determine if T-VEC solutions could find the hidden code bug that is the most likely cause of the Mars Polar Lander (MPL) crash.

  • Mars Polar Lander project started February 1994, lost on December 3,1999 after 11 months in space, traveled at least 35 million miles, cost of approx. $165 million, and only 40 meters from landing.
  • Premature engine shutdown most likely cause when Touchdown Monitor (TDM) software falsely indicated landing.
  • Verification activities were comprehensive and performed by dedicated, experienced engineers.
  • Fault not malicious, just difficult to finds.
  • According to Bob Knickerbocker (Director of Software at Lockheed Martin), Lockheed Martin had serendipitously found the bug a couple months after the crash.
  • The Problem
    Undiscovered code bug is likely cause of Mars Polar Lander crashs
  • The Approach
    Modeled textual requirements, generated tests and test drivers, and executed test
  • Implementation
    Apply T-VEC automated solution to model requirements, generate tests, and execute tests
  • Results
    T-VEC solutions identified code bug in fewer than 12 hours that is probable cause of failure