Re: [SystemSafety] Logic

From: Derek M Jones < >
Date: Tue, 18 Feb 2014 17:22:00 +0000


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
_______________________________________________
The System Safety Mailing List
systemsafety_at_xxxxxx
Received on Tue Feb 18 2014 - 18:23:19 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:06 CEST