Re: SPARK User Group 2008

["Michael" <Michael@home.ca>]

"Simon Wright" <simon.j.wright@mac.com> wrote in message
news:m21w42hqp8.fsf@mac.com...
 > If you are saying "if they don't do it right, it will be a failure" --
> well, duh, this is news?

OUCH, that sparks!


Being distracted by discussions is not focusing on safety.
March the 26th, 2006, BC ferries' Queen of the North vanished just like 
that!
"Crew had also turned off alarms that would have alerted them to danger."

Engineering is not that much about doing wrong or right, but knowing what is 
being done.

Even before a system gets operational, what matters is early identifying 
vulnerabilities, locating anomalies and resolving any deficiency prior a 
dysfunction occurs.  (i.e.: A clue: dysfunctions mostly occur in a specific 
context (not necessarily the current application domain), but anomalies are 
almost there! Without a trace? Not really!).

Apparently it wasn't one of the "Correctness by Construction" capabilities.
Therefore Praxis's iFACTS verifications never noticed any defects, but the 
NATS's iFACTS validation.
(i.e.: The 7 of March 2007, NATS news released proudly announced the iFACTS 
final trials.  Since, NATS never announced that iFACTS gets commissioned - 
find the errors! - anomalies I meant).

Like it says, "Correctness by Construction" is a brand new distilled set of 
formal principles, to realize systems and software engineering outputs with 
very low defect rate and very high resilience to change.

"Is Proof More Cost-Effective Than Testing?"
Or is CbC "just another way to make things so complicated that there are no 
obvious deficiencies?"

Praxis-HIS gets almost $20 millions to develop iFACTS and demonstrating that 
Formal method, formal verification and SPARK all together "appear to be 
substantially more efficient at finding faults than the most efficient 
testing phase".

Preliminary answers are expected at Ada Europe, in Venice, Italy, 16-20 
June.

Better to know how easily removable iFACTS deficiencies are!
If yes, did NATS reschedule iFACTS with new funding?

Cheers,

Michael,
Vancouver, BC

NOTE:
Never underestimate engineering capabilities:
Running without visibility, faster than you can and hitting the sound 
barrier is all but probable.
It's more likely going from your speed to zero in less than 1 second!

Big bang on the nose?

"Much ado about nothing" indeed.