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,ASCII Path: g2news1.google.com!postnews.google.com!11g2000prw.googlegroups.com!not-for-mail From: Claude Newsgroups: comp.lang.ada Subject: Re: What is SPARK about? Date: Wed, 16 Jun 2010 19:10:28 -0700 (PDT) Organization: http://groups.google.com Message-ID: <71a18ccd-6bfe-4ada-a78a-68206c334db8@11g2000prw.googlegroups.com> References: NNTP-Posting-Host: 70.79.53.248 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1276740628 29429 127.0.0.1 (17 Jun 2010 02:10:28 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 17 Jun 2010 02:10:28 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: 11g2000prw.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:11793 Date: 2010-06-16T19:10:28-07:00 List-Id: On Jun 12, 10:37=A0pm, "J-P. Rosen" wrote: > Claude a crit :> Feb 2010, the ERCIM Working Group on Formal Methods for = Industrial > > Critical Systems stated: =A0 There is a lack of precedents where formal > > methods have been proven to be effective. > >http://www.inrialpes.fr/vasy/fmics/ > > > Did the ECRIM overlook iFACTS? > > More surprisingly, did they overlook Meteor (100% automated line 14 of > the Parisian subway, in B+Ada) ? > > -- > --------------------------------------------------------- > =A0 =A0 =A0 =A0 =A0 =A0J-P. Rosen (ro...@adalog.fr) > Visit Adalog's web site athttp://www.adalog.fr Hello Jean-Pierre, ------------ http://www.bmethod.com/pdf/grace-2010/1-the-big-picture.pdf ------------ B into industrial existence (page 5): - turned out to be a real success: - 86 k loc software - still in v1.0 today, no bug detected so far B for systems: the reasons (page 8) - 100% proved software is not a guaranty per se - Even if METEOR ATP is still in v1.0 in 2010 - Ex: ATP reverse-engineered, from existing wired-logic systems to Programmable Logic Controller (PLC) - Not able to stop precisely at station - Software 100% proved but its specification was not the one that could make the train stopping ------------ 86 k loc to supersede wired-logic (e.g., Metro line D). That kind of Railway automated systems is about sequential logic and finite state machine. Therefore, that is right within the scope of formal methods. (A+) i.e., Since the specifications of the whole system (formerly wired- logic) could be expressed as a set of provable statements, automated tools were able to explicitly address the functional aspects of the specified behaviour. That might explain why the ERCIM Working Group on Formal Methods for Industrial Critical Systems was "Not able to stop precisely at the METEOR station" Next Station ... iFACTS?!??? Claude