From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,193117a6843a81b2 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news1.google.com!border1.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!pd7cy1no!pd7cy2no!shaw.ca!pd7urf3no.POSTED!53ab2750!not-for-mail X-Trace-PostClient-IP: 70.79.99.242 From: "Michael" Newsgroups: comp.lang.ada References: <9f80aed6-6509-4faf-931b-e05dc2b314d9@59g2000hsb.googlegroups.com> Subject: Re: SPARK User Group 2008 X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.3138 X-MIMEOLE: Produced By Microsoft MimeOLE V6.00.2900.3198 X-RFC2646: Format=Flowed; Original Message-ID: Date: Tue, 27 May 2008 18:43:05 GMT NNTP-Posting-Host: 64.59.144.74 X-Complaints-To: abuse@shaw.ca X-Trace: pd7urf3no 1211913785 64.59.144.74 (Tue, 27 May 2008 12:43:05 MDT) NNTP-Posting-Date: Tue, 27 May 2008 12:43:05 MDT Organization: Shaw Residential Internet Xref: g2news1.google.com comp.lang.ada:401 X-Original-Bytes: 4395 Date: 2008-05-27T18:43:05+00:00 List-Id: "Simon Wright" 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?