What I found more interesting was this section in the story of the Remote Agent bug ( http://ic.arc.nasa.gov/publications/pdf/2000-0176.pdf http://ic.arc.nasa.g

What I found more interesting was this section in the story of the Remote Agent bug ( http://ic.arc.nasa.gov/publications/pdf/2000-0176.pdf http://ic.arc.nasa.gov/publications/pdf/2000-0176.pdf ) One of the errors found with SPIN, a missing critical section around a conditional wait statement, was in fact reintroduced in a different subsystem that was not verified in this first preflight effort. This error caused a real deadlock in the RA during flight in space. So the bug fixed with the repl was actually one that was uncovered by the SPIN verifier ( http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html ) months prior to the launch, but wasn't fixed because they didn't verify the code they actually decided to use.