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

From: Roderick Chapman < >
Date: Mon, 04 May 2015 20:04:03 +0100

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


The System Safety Mailing List
systemsafety_at_xxxxxx Received on Mon May 04 2015 - 21:04:19 CEST

This archive was generated by hypermail 2.3.0 : Sun Feb 17 2019 - 20:17:07 CET