[SystemSafety] systemsafety Digest, Vol 34, Issue 5
Peter Bishop
pgb at adelard.com
Fri May 8 09:52:20 CEST 2015
On my calculations, your results imply there were 1896 conditions that
had to be assessed / proved manually.
We have done this type of manual review of tool output - though not for
SPARK - and it takes quite a while to review, assess and document (i.e.
measured in man-days).
How long did this assessment/proof stage take in your case?
Peter
Roderick Chapman wrote:
>
>
> On 04/05/2015 16:42, systemsafety-request at lists.techfak.uni-bielefeld.de
> wrote:
>> lots of memory.
> Derek's experience of strong static analysis may be based on
> retrospective analysis of badly written or unsubsetted C or C++,
> but that's nothing like our experience with SPARK.
>
> The key is modularity and contracts in the programming language - get
> that right, and the rest falls into place. (Hint: start with a programming
> language which actually _has_ a module system... :-) ) Modularity
> also gets us the ability to aggressively parallelize the theorem-proving
> work, so the more processor cores you can throw at it the better...
>
> Here's some data for an operational build of the NATS iFACTS
> system, published in our keynote at the ITP conference
> last year. The analysis basically shows that the software
> is "type safe" - meaning no crashes, no undefined behaviour, and
> no exceptions (including all buffer overflows, arithmetic overflows,
> range violations, and division by zero.)
>
> Size: 250kloc logical of SPARK (measured by GNATMetric)
>
> Verification Conditions: 152927
>
> Completeness 98.76% are proven completely automatically
> by the "out of the box" SPARK toolset. The remainder are
> proved with either the addition of user-defined lemmas
> to help the prover or manual review.
>
> Proof time: 3 hours, starting from scratch, or about 15
> minutes average for a small change with persistent caching of the
> proof results from an earlier run.
>
> In short - we're down to "coffee break" timescales to re-prove
> the whole thing, so the developers always re-run the proof
> _before_ the commit any change to the CM system.
>
> This is all done on desktop class machines, or a single
> server that costs about £2k today (16 processor cores and
> about 32GB RAM...nothing special at all...)
>
> More metrics from other projects are in the paper, PDF of
> which is on www.proteancode.com
>
> - Rod
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
--
Peter Bishop
Chief Scientist
Adelard LLP
Exmouth House, 3-11 Pine Street, London,EC1R 0JH
http://www.adelard.com
Recep: +44-(0)20-7832 5850
Direct: +44-(0)20-7832 5855
More information about the systemsafety
mailing list