[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