Re: SPARK User Group 2008

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

"Simon Wright" <simon.j.wright@mac.com> wrote in message 
news:m2iqx1z8fe.fsf@mac.com...

> But see 
> http://www.airflights.co.uk/news/default.aspx?category=438006664&story=18081798&archive=-&AspxAutoDetectCookieSupport=1

Nice picture!

Thank you Simon, your contribution is greatly appreciated.

Did you also notice your finding was posted: Wed, 07 Mar 2007 14:53:47 GMT,
That's a few minutes after NATS proudly announced the iFACTS final trials.

In other words you just confirm the problem: iFACTS has vanished after the 
NATS's final trial and no one can say what the problems were.
(Since UK air traffic is still growing, delay is the safety problem)


Such problem seems to emanate from a UK military standard (00-55)
Requirements for safety related software in defence equipment - 1st August 
1997.
"The testing shall exercise all properties and functions which have not been 
demonstrated by formal verification."
http://www.dstan.mod.uk/data/00/055/01000200.pdf

Since CbC is just about formal methods, as per standard 00-55, iFACT 
reliability was merely demonstrated by formal verification.

No testing means no visibility on problems, not even a doubt it might have 
any problem.

e.g.: "Crew had also turned off alarms that would have alerted them to 
danger."


WHAT ENGINEERING SAYS:
"Formal verification will not make complex systems simple either. There is 
no magic here. Some limitations of formal verification include that the 
system of formal mathematics, such as proofs, may be larger than the program 
being verified. Often, the formal verification is very difficult to 
construct. Like anything difficult to construct, it is likely to contain 
errors. Some limited aspects of system behavior may be proven, but are these 
errors likely to be caught in testing anyway? Are these errors ones that are 
likely to cause accidents? Formal verification probably has little effect on 
safety unless it is aimed at the safety constraints."


In facts, the iFACTS fiasco was predictable before the iFACTS project even 
begins.

With some unit and non-regression testing, iFACTS divergences would have 
been early detected.
i.e.: iFACTS would have had a chance to be commissioned, and another safety 
risk could have been addressed.

http://seattletimes.nwsource.com/html/travel/2004128412_webaircanada16.html
e.g.: January the 10th, 2008, over BC, "Wake from passing plane may have 
caused Air Canada jet's plunge: 10 passengers injured."
i.e.: Medium Term Conflict Detection strongly needed, but not iFACTS.

Cheers,
Michael, BC


NOTES:
In 2006, an integrated product team comprising NATS, Lockheed Martin and 
Praxis launched the interim Future Area Control Tools Support (iFACTS) 
system,
http://www.lockheedmartin.com/products/london-area-control-center/index.html

March 12, 2007 - iFACTS poised to transform ATC:
"Praxis managing director Keith Williams says that, at present, the system 
is "85% of the way to being operational",
http://www.tmcnet.com/usubmit/2007/03/12/2407775.htm

SigAda 2007 - Fairfax, Virginia, USA, November 4-9, 2007 - as usual, 
Praxis-HIS proudly presented CbC
http://www.sigada.org/conf/sigada2007/

Next Ada Europe, Venice, Italy, 16 - 20, June 2008 - CbC is gone (embroglio 
or fiasco?)
http://www.math.unipd.it/ae2008/
SIGAda 2008: Portland, Oregon, USA, October 26-30, 2008 - is CbC yet coming?