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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b03962e55f213a92 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,CP1252 Path: g2news1.google.com!postnews.google.com!a39g2000prb.googlegroups.com!not-for-mail From: Claude Newsgroups: comp.lang.ada Subject: Re: What is SPARK about? Date: Sat, 12 Jun 2010 11:09:48 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: NNTP-Posting-Host: 70.79.53.248 Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1276366188 28075 127.0.0.1 (12 Jun 2010 18:09:48 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sat, 12 Jun 2010 18:09:48 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: a39g2000prb.googlegroups.com; posting-host=70.79.53.248; posting-account=WPcl4AoAAAC3CTqLAgWnftzSSCqiCJ4J User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.3) Gecko/20100401 Firefox/3.6.3,gzip(gfe) Xref: g2news1.google.com comp.lang.ada:11662 Date: 2010-06-12T11:09:48-07:00 List-Id: On Jun 12, 1:30=A0am, Phil Thornley wrote: > On 11 June, 21:32, Claude wrote: > > > Ada is a formal language to software engineering. > > > What is SPARK about? > > SPARK is an annotated sublanguage of Ada, intended for use in high- > integrity applications. Annotations (Ada comments) and Ada source code compose the SPARK semantic, which shall fly together on the SPARK tools in order to determine and discharge any Verification Condition. (Static analysis completeness is the SPARK programming goal). (Ada=92s generic and variant records are within static analysis=92s capabilities but still on the SPARK =93road map=94) > An important property of the language is that it is unambiguous - > every valid SPARK program, when compiled by a conforming Ada compiler, > has one and only one meaning. Ada source code (constrained to be unambiguous, from SPARK static analysis) shall fly alone on the Ada compiler, like the Ada executable will on the target system. (Functional behaviour compliance is the Ada engineering goal, assisted by the SPARK guidelines). > Therefore it becomes practicable to reason about the behaviour of a > SPARK program based solely on the analysis of the program text. Annotations are the static analysis directives to be established by Software Engineers to increase the software product likelihood to behave as intending, and reduce risks of error to an acceptable level. > > I means since SPARK is restricted to the best of Ada, is SPARK better > > than Ada to resolving complex engineering applications, or SPARK a > > better choice than C/C++ to address leaner systems? =A0(in terms of > > compliance to early drafts of DO-178C - certification levels C to A). > > > Indeed, the successful applications of SPARK bring to results that are > > rather difficult to compare. > > > =93The formal design of Tokeneer ID Station (TIS) shows the TIS system > > to be a purely sequential system.=94 - =A0(INFORMED design, at section > > 2.2, Identification of the SPARK boundary) > > Support for concurrent programs (RavenSPARK) was added in 2003. (Tokeneer was also on how to accede the administrator and user ID station simultaneously). Rather, =93Purely sequential system=94 doesn't refer to single task, but to the =93sequential logic of a finite state machine=94. That is what Tokeneer is, and what the INFORMED design means. Therefore, Tokeneer was fairly straight forward to prove, just a little was done and everything worked! > > =93We believe part of the success of proof on SHOLIS is due to the > > simple system architecture. =85 > > Some large-scale SPARK reasoning are also needed, including support > > for abstract proof, before the technology can be extensively used at > > the highest level of large systems.=94 - (Is Proof More Cost Effective > > Than Testing =96 Section 8, Summary). > > Support for abstract proof was added in 2000. > > > > > Beyond any theory or academic project, 10 years later, from all the > > past SPARK projects=92 experiences, does it happen that SPARK can > > address =93purely sequential systems=94 or that SPARK =93can be extensi= vely > > used at the highest level of large systems=94? > > An example of a large, concurrent SPARK program is iFACTS - described > by the UK National Air Traffic Service as "the biggest change in air > traffic control since radar". Feb 2010, the ERCIM Working Group on Formal Methods for Industrial Critical Systems stated: =93There is a lack of precedents where formal methods have been proven to be effective.=94 http://www.inrialpes.fr/vasy/fmics/ Did the ECRIM overlook iFACTS? Formal Methods (i.e., Z notation and SPARK) are best suited to the development of data oriented, sequential systems. i.e., they are generally sufficient to demonstrate data flow correctness and SPARK can prove the absence of run time error. But on how to handle the functional complexities of large systems, they had always led to dead ends, almost. > > Claude > > Cheers, > > Phil iFACTS: What has been accomplished there? Does the abstract proofs were able to consider and address all functional validations? Were traditional testing involved and did they do all the functional verification: (over data flow correctness and proof of absence of run time error)? ------------------------------------------------------ There are boundaries there, which need to be clarified. ------------------------------------------------------ Thanks Phil Claude