[SystemSafety] Logic

[Derek M Jones]

Martyn

>> Having a few bodies in a corner office working on formal methods
>> is small scale, just because they are part of a large project does
>> not make the use large scale.
>
> Derek
>
> I agree - but why do you assume that such was the case?

Experience has given me a very jaded view of the claims made by
proponents of formal methods.

I think a cost/benefit analysis of formal methods could well
come out in favor of their use for very critical code, such
as the software controlling the safety rods in a nuclear power
plant.

> Please define what you would consider to be large enough. Please tell me
> what you would regard as /just/ big enough to be a counterexample to
> your statement that

It is possible to write large quantities of 'code' in some formal method
language.  The ISO Modula-2 Standard is 600+ pages long and almost all
formal notation.  But as far as I know the only 'formal' tool they used
involved the layout of the text.

If you define formal methods as writing the formal 'code' and proving
something useful with it, then

    o what is considered to be an adequate proof?
Issues and links to interesting papers here:
http://shape-of-code.coding-guidelines.com/2013/11/17/what-is-the-error-rate-for-published-mathematical-proofs/

    o what is useful?
That is for the customer to say.

I don't have any references to cost vs length of formal proofs;
compute resources (i.e., time) vs length of formal proof is also
another issue for which data is very sparse and vague.

I know of cases where a few hundred lines have been analysed
using formal methods to a degree that looks very solid.

Thousands of lines?  The nicta work I talk about here:
http://shape-of-code.coding-guidelines.com/2012/05/23/would-you-buy-second-hand-software-from-a-formal-methods-researcher/ 

is in this ball park, but they assumed to much and I was not
convinced.

The analysis of the Viper processor springs to mind as an example
of something non-trivial.  I know there was lots of debate about
that worked had actually proved and what constitutes correctness.
There is an excellent article discussing this that I cannot find
the link to at the moment.

I know of projects that started off using formal methods and found
them too expensive for the benefits provided and also found they
made it difficult to substantially change the software later (because
the need to redo the formal side would have been prohibitive).

So my view is that formal methods may scale to a few thousand lines,
provided the code is not likely to substantially evolve over time (or
the money is available for major reworking of the formal side).

-- 
Derek M. Jones                  tel: +44 (0) 1252 520 667
Knowledge Software Ltd          blog:shape-of-code.coding-guidelines.com
Software analysis               http://www.knosof.co.uk