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

From: David MENTRE < >
Date: Thu, 27 Feb 2014 14:09:09 +0100


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



The System Safety Mailing List
systemsafety_at_xxxxxx Received on Thu Feb 27 2014 - 14:09:21 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:06 CEST