> You make it seem like the formal verification missed an issue.
Sorry, that was not my intent. I added a clarification.
> > You make it seem like the formal verification missed an issue.
> Sorry, that was not my intent. I added a clarification.
I'm sorry but it didn't. Without reading next comment I wouldn't know why it failed.
"The first effort consisted of analyzing part of the RA autonomous space craft software using the SPIN model checker. 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 pre-flight effort. This error caused a real deadlock in the RA during flight in space."
The model actually found an issue that was later reintroduced in a different part of the system that was not formally verified. If anything, it tells us we need _more_ formal verification!