Re: [SystemSafety] systemsafety Digest, Vol 34, Issue 5

From: Peter Bishop < >
Date: Fri, 08 May 2015 08:52:20 +0100


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_xxxxxx > 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_xxxxxx
-- 

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
_______________________________________________
The System Safety Mailing List
systemsafety_at_xxxxxx
Received on Fri May 08 2015 - 09:52:41 CEST

This archive was generated by hypermail 2.3.0 : Fri Feb 22 2019 - 05:17:07 CET