[SystemSafety] Data on Proof effectiveness from real projects

From: David MENTRE < >
Date: Wed, 30 Mar 2016 08:39:28 +0200

Hello Roderick,

Le 22/03/2016 13:19, Roderick Chapman a écrit :
> The best summary of SPARK projects is in our keynote paper from
> ITP 2014.
I already read this one.

> There's also
> good data on the C130J in Andy German's article in CrossTalk,

Also read it. :-)

> and in Jim Sutton's "Lean Software Strategies" book.
> Oh...there's also the MULTOS CA project - the data is in IEEE
> Software, Jan/Feb 2002.

Don't know those, I'll look at them.

And there is also King et al. paper "Is proof More Cost Effective than Testing?" on SHOLIS project.

Interestingly, for SHOLIS the efficiency of fault detection was, in decreasing order, "Z proof" (i.e. spec proof), "System Validation" (i.e. System tests), "Integration Test", Code proof and "Acceptance" (client tests?) and Unit test. This illustrates well that the best approach is a mix of test (especially for integration and validation) and proof (especially at spec level, very efficient, but code proof is also more efficient that unit test). Of course, as Matthew said, I should not generalize too much from some samples.

But I definitely need to take some time to re-read all those papers.

Thanks Roderick!
Best regards,

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Wed Mar 30 2016 - 08:39:39 CEST

This archive was generated by hypermail 2.3.0 : Sat Feb 23 2019 - 10:17:08 CET