[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