[SystemSafety] Bursting the formal methods bubble

[Derek M Jones]

jean-louis,

> I thinks that we have more example of mistake in classical development that
> in formal development

This is because there is so little formal development, we
don't have enough data to reliably say one way or the other.

> yes all method are applied by human and error appear but with formal
> methods you have a tool to detect it.

There are tools to detect mistakes in code (not that these are widely
used :-(

> with ADA, C .... C++ or JAVA and C# its more difficult to develop a
> software with a very low level of bug ...

If you do multiple implementations, e.g., Ada+formal or
Ada+Visual basic, you will detect more problems and the result will
be more reliable software.

The important question is bugs (or lack of) per buck.
Which technique is the most cost effective?

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com