Re: [SystemSafety] Claims for formal methods

From: Peter Bishop < >
Date: Thu, 20 Feb 2014 13:58:32 +0000

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

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_xxxxxx

> C. Michael Holloway, speaking only for himself and not his organiztion
> --
> /*cMh*/
> ------------------------------------------------------------------------
> _______________________________________________
> The System Safety Mailing List
> systemsafety_at_xxxxxx

Peter Bishop
Chief Scientist
Adelard LLP
Exmouth House, 3-11 Pine Street, London,EC1R 0JH
Recep:  +44-(0)20-7832 5850
Direct: +44-(0)20-7832 5855
The System Safety Mailing List
Received on Thu Feb 20 2014 - 14:58:42 CET

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