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,55ae3803eb91d6ca X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news1.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post01.iad.highwinds-media.com!newsfe17.iad.POSTED!7564ea0f!not-for-mail From: "Michael" Newsgroups: comp.lang.ada References: Subject: Re: Ada UK conference: SPARK safety: is no delivery better than 1 defect? X-Newsreader: Microsoft Outlook Express 6.00.2900.5512 X-MIMEOLE: Produced By Microsoft MimeOLE V6.00.2900.5579 X-RFC2646: Format=Flowed; Original Message-ID: NNTP-Posting-Host: 174.6.150.104 X-Complaints-To: internet.abuse@sjrb.ca X-Trace: newsfe17.iad 1236854225 174.6.150.104 (Thu, 12 Mar 2009 10:37:05 UTC) NNTP-Posting-Date: Thu, 12 Mar 2009 10:37:05 UTC Date: Thu, 12 Mar 2009 03:36:58 -0700 Xref: g2news1.google.com comp.lang.ada:4062 Date: 2009-03-12T03:36:58-07:00 List-Id: Hi Bill and all, iFACTS has failed as an engineering results. Engineers are used to find solutions rather than excuses (i.e.: former SPARK successful software development process involves substituting testing by formal proofs; and the iFACTS managers were confident that proven procedures were used in dealing with problems. In case of problem, changing the way engineering must be done is a necessity for engineers to report). Tokeneer is an open project, so open for discussion: My initial question was: "In regards to the Tokeneer mini-project findings, were the safety critical iFACTS project's delays and deficiencies predictable?" A few months prior NATS realised iFACTS was ending with a lot of deficiencies, Praxis and NATS were still celebrating a great iFACTS success story (just prior the final iFACTS trials at Hurn). "Paul Barron, NATS' Chief Executive commented: "This is one of the most exciting developments in the aviation industry in decades and we're now close to introducing it." http://www.praxis-his.com/news/radarmar2007.as http://www.nats.co.uk/uploads/user/NERL%20Business%20Plan%20Report%202008.pdf page 6 "In all engineering disciplines it is accepted that it is better to avoid the introduction of errors rather than have to correct them at a later stage." How "correctness per construction" fails to meet such a fundamental goals? Pre-condition: there must have no effective validation or verification procedure. It might be a few known limitations: e.g.: SPARK can ensure intrinsic code robustness, but not the software compliance toward system specifications. But there if were enough deficiencies to avoiding iFACTS to converge to a compliant solution, there were enough for SPARK to catch. And SPARK, as well as that the Z formal specifications, caught none of them. What's the SPARK problem? Good enough for Tokeneer, blind as a bat for iFACTS! The next Ada UK Conference is still a responsibilities for Rod Chapman and Janet Barnes to clarifying the Praxis's SPARK capabilities (Tookeneer) and limitations (iFACTS). In 2007, conclusion of "Correctness by Construction: Putting Engineering into Software" was quite amazing: http://www.adacore.com/multimedia/aa_videos/lectures/adauk07_05_slides.pdf "A future? What happens if we put together: - ... - CbyC, - SPARK and strong static verification, Don't know! But we aim to have some fun finding out." Have fun, Cheers Michael, Vancouver, BC CC: to Rod Chapman and Janet Barnes Just in case: Formal specifications can describe in a precise way the properties of an information system, but without constraining the software architecture and design in which these properties are to be achieved. In others word formal specifications describe what the system must do without saying how it is to be done. Therefore, formal specifications are the mathematical foundation which can ensure system requirements shall be transformed into consistent and accurate systems specifications. 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, ultimately preventing system instability, saturation or even crash.