[SystemSafety] Data on Proof effectiveness from real projects

David MENTRE dmentre at linux-france.org
Wed Mar 30 08:39:28 CEST 2016


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,
david


More information about the systemsafety mailing list