[SystemSafety] systemsafety Digest, Vol 34, Issue 5

[Steve Tockey]

Can static analysis catch this kind of defect:

https://www.ima.umn.edu/~arnold/disasters/patriot.html


Cheers,

-- steve



From: jean-louis Boulanger <jean.louis.boulanger at gmail.com<mailto:jean.louis.boulanger at gmail.com>>
Date: Monday, May 4, 2015 1:03 PM
To: Roderick Chapman <roderick.chapman at googlemail.com<mailto:roderick.chapman at googlemail.com>>
Cc: "systemsafety at lists.techfak.uni-bielefeld.de<mailto:systemsafety at lists.techfak.uni-bielefeld.de>" <systemsafety at lists.techfak.uni-bielefeld.de<mailto:systemsafety at lists.techfak.uni-bielefeld.de>>
Subject: Re: [SystemSafety] systemsafety Digest, Vol 34, Issue 5

In the book "static analysis", I presented some trues experiences from railway and aeronautics with POLYSPACE, ASTREE and FRAMAC on industrial applications (from AIRBUS, DASSAULT and THALES) with very good results.
in the example from THALES we replaced unit test and some integration tests by static analysis and properties verification ...
in this application in C (pointer, complex data structures, one master and slave application produce by the same C code (used of #define) ...)
it worked and it's possible to apply it to any code ... see the new DO 178 and the formal method book ...

2015-05-04 21:04 GMT+02:00 Roderick Chapman <roderick.chapman at googlemail.com<mailto:roderick.chapman at googlemail.com>>:


On 04/05/2015 16:42, systemsafety-request at lists.techfak.uni-bielefeld.de<mailto: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<http://www.proteancode.com>

 - Rod


_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE<mailto:systemsafety at TechFak.Uni-Bielefeld.DE>



--
Mr Jean-louis Boulanger
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20150504/5f7d7c1c/attachment.html>