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,LOTS_OF_MONEY 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!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!nx02.iad01.newshosting.com!newshosting.com!64.59.134.4.MISMATCH!pd7cy3no!pd7cy4no!shaw.ca!pd7urf1no.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: Sun, 25 May 2008 20:14:38 GMT NNTP-Posting-Host: 64.59.144.74 X-Complaints-To: abuse@shaw.ca X-Trace: pd7urf1no 1211746478 64.59.144.74 (Sun, 25 May 2008 14:14:38 MDT) NNTP-Posting-Date: Sun, 25 May 2008 14:14:38 MDT Organization: Shaw Residential Internet Xref: g2news1.google.com comp.lang.ada:345 Date: 2008-05-25T20:14:38+00:00 List-Id: "Simon Wright" 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.