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

[David MENTRE]

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?

* Two first examples:

    1. Subway line 14 in Paris (project end: 1998)

    2. Roissy Airport Shuttle (project end: 2006)

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.


* Another example: New York Canarsie Line CBTC (project end: ~2006).

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).

   * Software requirements formalisation: 4 persons over 7 months (28
man.month)

   * Refinement to ADA code: 3 persons over 3 months (9 man.month)

   * (Interactive) Proof: 3 persons over 3 months (9 man.month)

   * Functional test: 3 persons over 3 months (9 man.month)

Sources:
  * Formal Methods in Industry: Achievements, Problems, Future. 
Jean-Raymond Abrial, ICSE'06.

  * B in Large-Scale Projects: The Canarsie Line CBTC Experience. Didier 
Essamé and Daniel Dollé, B 2007, LNCS 4355.


Sincerely yours,
D. Mentré