[SystemSafety] systemsafety Digest, Vol 66, Issue 5
Derek M Jones
derek at knosof.co.uk
Thu Jan 4 15:15:36 CET 2018
Rod,
Does "100% OK" mean that 2 faults per thousand lines of code
are OK?
This is the fault rate found in the paper:
"Tokeneer: Beyond Formal Program Verification"
www.open-do.org/wp-content/uploads/2010/04/ERTS2010_final.pdf
> the SPARK theorem prover ... the teams at Altran use "proof
> completeness" (i.e.
> essentially the false alarm rate of the prover) as a pre-commit target.
> Bottom line -
> either the theorem prover says your code is 100% OK with no false
> alarms, or it doesn't
> go into CM.
--
Derek M. Jones Software analysis
tel: +44 (0)1252 520667 blog:shape-of-code.coding-guidelines.com
More information about the systemsafety
mailing list