[SystemSafety] Claims for formal methods

[Peter Bishop]

I concur with Michael and Heath. This is an open forum, and there will 
be disagreements from time to time. In that case the best response
is to demand evidence to back up any claims we make
- and that goes for both sides of the argument.

 From my point of view there is no doubt about the logical underpinnings 
of the formal approach.

The issue in dispute is over the scope and practical applicability of 
formal methods.

Could we agree on the following?

1. Formal proofs are not an absolute guarantee of correctness.
There can be doubts about the language semantics, the proof engine, the 
translation to binary and the hardware.

2. They don;t necessarily address the requirements problem, though 
modelling the problem space in conjunction with a formal requirements 
description can help here.

3. They are not so good for non-functional properties like real time 
response, dynamic stability etc. which can be extremely important from a 
safety perspective.

Nevertheless my experience with assessing real-time embedded devices is 
that formal methods are valuable for verifying specific properties 
(especially safety properties) at the requirements level and for partial 
proofs of functionality at the code level for portions of code that are 
safety-critical.

Peter Bishop
Adelard

C. Michael Holloway wrote:
>   Not that my opinion need matter much, but I concur fully with Mr. 
> Raftery.  Editing the archive is a blight on the integrity of the list.  
> In some ways, doing so seems worse to me than anything Mr. Jones wrote.
> 
> On 2/19/14 6:08 PM, Heath Raftery wrote:
>> ...
>> That would be a real blight on the impartiality of this list. You're 
>> entitled to censor the service as you wish, but removing criticism of 
>> the establishment would represent a dramatic drop in the integrity I 
>> perceive this resource to present.
>>
>> I'm not going to put up any fight, but wanted to offer a different 
>> viewpoint to your own.
>>
>> Heath
>>
>> _______________________________________________
>> The System Safety Mailing List
>> systemsafety at TechFak.Uni-Bielefeld.DE
>>
> C. Michael Holloway, speaking only for himself and not his organiztion
> 
> -- 
> /*cMh*/
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE

-- 

Peter Bishop
Chief Scientist
Adelard LLP
Exmouth House, 3-11 Pine Street, London,EC1R 0JH
http://www.adelard.com
Recep:  +44-(0)20-7832 5850
Direct: +44-(0)20-7832 5855