[SystemSafety] Formal methods scalability, some real-world figures (was: Logic)

From: David MENTRE < >
Date: Thu, 20 Feb 2014 09:42:33 +0100

Hello Mr Jones,

Le 18/02/2014 18:22, Derek M Jones a écrit :
> I don't have any references to cost vs length of formal proofs;
> compute resources (i.e., time) vs length of formal proof is also
> another issue for which data is very sparse and vague.
> I know of cases where a few hundred lines have been analysed
> using formal methods to a degree that looks very solid.
> So my view is that formal methods may scale to a few thousand lines,
> provided the code is not likely to substantially evolve over time (or
> the money is available for major reworking of the formal side).

Use of formal methods does scale to at least hundred of thousands lines of code (at least up to 158,000 lines of code).

Here are below three examples using B Method (http://www.methode-b.com/en/), using Atelier B tool (http://www.atelierb.eu/en/), with associated cost figures (to answer your above question). In those three examples coming from subway/light rail systems, both on-board and side-way software have been formalized.

In the below examples, of course, not all functional properties have been formally verified, only those relevant to safety critical functionalities. But this is the relevant part, wouldn't you agree?

In case 1: 86,000 lines of Ada produced; 27,800 proof obligations; 8.1% of interactive proofs; 7.1 man.month of interactive proof time.

In case 2: 158,000 lines of Ada produced; 43,610 proof obligations; 3.3% of interactive proofs; 4.6 man.month of interactive proof time.

The software is bigger that the previous projects, for example the on-board vital software of Canarsie CBTC is bigger that ALL vital software (on-board + wayside) of Paris subway line 14 (i.e. > 86,000 lines of code).


Sincerely yours,
D. Mentré

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Thu Feb 20 2014 - 09:42:47 CET

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