[SystemSafety] Claims for formal methods

[RICQUE Bertrand (SAGEM DEFENSE SECURITE)]

We should not mind that much about wording as long as don't have ad hominem issues. I feel disappointed when people take absolutely everything too serious. We can have serious discussion while keeping the formalism rather open to humour, causticity, irony, teasing questions, etc... Persons have also the right to go too far if it is later acknowledged.

Bertrand Ricque
Program Manager
Optronics and Defence Division
Sights Program
Mob : +33 6 87 47 84 64
Tel : +33 1 59 11 96 82
Bertrand.ricque at sagem.com



-----Original Message-----
From: systemsafety-bounces at lists.techfak.uni-bielefeld.de [mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] On Behalf Of Peter Bishop
Sent: Thursday, February 20, 2014 2:59 PM
To: C. Michael Holloway
Cc: systemsafety at lists.techfak.uni-bielefeld.de
Subject: Re: [SystemSafety] Claims for formal methods

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
_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE
#
" Ce courriel et les documents qui lui sont joints peuvent contenir des informations confidentielles, être soumis aux règlementations relatives au contrôle des exportations ou ayant un caractère privé. S'ils ne vous sont pas destinés, nous vous signalons qu'il est strictement interdit de les divulguer, de les reproduire ou d'en utiliser de quelque manière que ce soit le contenu. Toute exportation ou réexportation non autorisée est interdite Si ce message vous a été transmis par erreur, merci d'en informer l'expéditeur et de supprimer immédiatement de votre système informatique ce courriel ainsi que tous les documents qui y sont attachés."
******
" This e-mail and any attached documents may contain confidential or proprietary information and may be subject to export control laws and regulations. If you are not the intended recipient, you are notified that any dissemination, copying of this e-mail and any attachments thereto or use of their contents by any means whatsoever is strictly prohibited. Unauthorized export or re-export is prohibited. If you have received this e-mail in error, please advise the sender immediately and delete this e-mail and all attached documents from your computer system."
#