From: Claude on
On Jun 12, 10:37 pm, "J-P. Rosen" <ro...(a)> 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.
> >
> > 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...(a)
> Visit Adalog's web site at

Hello Jean-Pierre,

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?!???

From: Claude on
On Jun 12, 12:27 pm, Yannick Duchêne (Hibou57)
<yannick_duch...(a)> wrote:
> Le Sat, 12 Jun 2010 20:09:48 +0200, Claude <claude.def...(a)> a  
> écrit:> 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.
> Sure there is way to... (it must be)

Once Peter Amey (prime author of SPARK Examiner) stated:
"what can be achieved is limited by precision of descriptions and
notations used".
"What we can achieve depends on the properties of the language we are
(ref: IEC 61508-conformant software development with SPARK)

The language is Ada. With that there is a long list of successfully
implemented large complex safety critical systems.
The SPARK tools are Prolog applications. With that there is a lot of
expert systems, and theorem proving applications.
Formal methods have been advocated as a means of increasing the
reliability of systems.

Puting it together, what can we do? Data flow control and code
properties verification...

Therefore, how Formal Methods can address the functional aspect of the
system behaviour?

The behaviour of reactive systems is largely conditioned by the
interaction with events of the external environment the
sequentialization of which is not predictable. The complexity of the
systems' behaviour increases considerably when the timing dependencies
in the execution of events are taken into account.
The above features are typical of a large class of systems including
control systems, automation systems, and communication systems and
results in the extreme difficulty of the verification of their

How Formal Methods can assess unpredictable sequentialization,
dependencies, complexity, and achieves that "extreme difficulty of the
verification of correctness."?

Phil Thornley, said that iFACTS could be part of the answer.

But, on what SPARK is about, the uncertainty stays still...

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.

> Sorry for being a bit out of topic, I would like to ask you a question, as  
> it seems you know about the state of the art. Please, do you know if there  
> are accessible documents about balancing intuitionistic logic vs classical  
> logic in this area ?

My knowledge is mostly founded on experiences.
But I know that Peter Amey was relating to "Bayesian mathematics" as
the limits what could be claimed from statistical testing.
"Bayesian probability interprets the concept of probability as "a
measure of a state of knowledge", in contrast to interpreting it as a
frequency or a physical property of a system."

Claude Defour