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 ) months prior to the launch, but wasn't fixed because they didn't verify the code they actually decided to use.
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 ) months prior to the launch, but wasn't fixed because they didn't verify the code they actually decided to use.