Re: What is SPARK about?

[Claude <claude.defour@orange.fr>]

On Jun 12, 10:37 pm, "J-P. Rosen" <ro...@adalog.fr> wrote:
> Claude a crit :> Feb 2010, the ERCIM Working Group on Formal Methods for Industrial
> > Critical Systems stated:   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) ?
>
> --
> ---------------------------------------------------------
>            J-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