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!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!nx01.iad01.newshosting.com!newshosting.com!64.59.134.4.MISMATCH!pd7cy3no!pd7cy4no!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: <6_UVj.133316$rd2.100938@pd7urf3no> Date: Mon, 12 May 2008 10:29:22 GMT NNTP-Posting-Host: 64.59.144.74 X-Complaints-To: abuse@shaw.ca X-Trace: pd7urf3no 1210588162 64.59.144.74 (Mon, 12 May 2008 04:29:22 MDT) NNTP-Posting-Date: Mon, 12 May 2008 04:29:22 MDT Organization: Shaw Residential Internet Xref: g2news1.google.com comp.lang.ada:48 Date: 2008-05-12T10:29:22+00:00 List-Id: Is the iFACTS project going to be an Ada success story? iFACTS is an engineering project made without engineering. That should have been a must, for a Medium Term Conflict Detection software conceived to enhance ATC operations and assist the UK flight controllers in assuring safety. Results are delays and an unusual amount of deficiencies. Some Ada projects are like that: ignoring the engineering for the sake of Ada. Ensuring system safety, stability and non-saturation are ones of the main engineering challenges. Ada is an engineering tool made to meet such objectives; and it works pretty well if used with the best software engineering practices and processes (i.e: SEI's CMM level III and over). SPARKS is a subset of Ada. The general goal of SPARK is to provide a language which increases the probability of the software code behaving as intending. In another word SPARK provides additional information, which allows performing rigorous mathematical analysis in order to significantly increase the code intrinsic integrity and runtime correctness. The benefits are to reduce the risk of processing erroneous data, and then preventing any error handling and/or system recovering risk. SPARKS has its advantages and its limitations. It better works for small embedded projects like airborne systems. Praxis-Hight Integrity Systems should have been well advised to favour High Engineering Reliability. That's still not sufficient for safety, but better than nothing (i.e: iFACTS). Cheers, Michael Vancouver