[SystemSafety] Scalability of Formal Methods [was: Logic]

[David MENTRE]

Hello Peter,

Le 26/02/2014 22:33, Peter Bernard Ladkin a écrit :
> I spent some time this afternoon looked at the work to which David
> referred, the ClearSy application of Atelier B to the Flushing line
> (he said Canarsie, but I only found details of Flushing) signalling
> systems.

Canarsie and Flushing are two different projects, also both are using B
Method.

Canarsie is a software development project, ultimately producing Ada
source code for on-board and way side equipments. It is similar to Paris
Line 14 or Orlyval.

Flushing
(http://www.methode-b.com/en/2013/07/system-level-formal-proofs-cbtc-new-york-flushing/
, some interesting slides can be found at
http://www.clearsy.com/wp-content/uploads/BFlushing26_en.pdf) is, as you
said, a system development project. Its main objective is to show that
the Thales CBTC specification and design are safe. They have derived
main safety properties ("trains should never collide", ...) into 
component level properties. The main result is paper, it is their "Book 
of assumptions" that makes explicit the design of all part of the system
(write on paper all the assumptions and the reasoning), even for
previously established rules like signalling rules. This work is formal,
but mainly with paper and pen proofs. The B Method was only used in a
second step to mechanically check the proofs and debug them. No code was
produced.

[ For Flushing ]
> In other words, the claims made about the system are too general for
> an expert to figure out what has actually been accomplished; what
> the demonstrated properties of the final system are.

 From ClearSy presentation, the aim of this work was precisely to make a
report allowing the local experts to figure out what has been 
accomplished and understand the reasoning down to basic (or not so 
basic) assumptions (physical, mechanical, CBTC algorithm, ...).

It is up to traditional development process to check that those 
assumptions are fulfilled.

Best regards,
david