[SystemSafety] Bursting the anti formal methods bubble

[Philippa Ryan]

Hi,

> On 8 Nov 2017, at 07:59, systemsafety-request at lists.techfak.uni-bielefeld.de wrote:
> 
> Message: 1
> Date: Tue, 7 Nov 2017 12:36:48 +0100
> From: David MENTR? <David.MENTRE at bentobako.org <mailto:David.MENTRE at bentobako.org>>
> To: systemsafety at lists.techfak.uni-bielefeld.de <mailto:systemsafety at lists.techfak.uni-bielefeld.de>
> Subject: Re: [SystemSafety] Bursting the anti formal methods bubble
> Message-ID: <57fa5e13-16e6-9ad0-17cf-1ead8d0bb195 at bentobako.org <mailto:57fa5e13-16e6-9ad0-17cf-1ead8d0bb195 at bentobako.org>>
> Content-Type: text/plain; charset=windows-1252
> 
> Dear Mr Bishop,
> 
> Le 2017-10-30 ? 11:01, Peter Bishop a ?crit?:
>> I think the discussion in this list illustrates the fact that FM (as
>> normally defined) is not a panacea.
> 
> I strongly agree. Nonetheless...
> 
>> It can be used for assuring correct implementation of functionality, but
>> is not so good for other key features of real time embedded systems, e.g.
> 
> ... you can find tools on the market to ensure such properties.
> 
>> - meeting timing requirements
> 
> AbsInt's aiT WCET Analyzers can be used to do such WCET analysis using FM:
> 
>  https://www.absint.com/ait/ <https://www.absint.com/ait/>

This isn’t quite what is being asked for though - having a WCET value doesn’t mean you have met your timing requirements. It could be over your requirement. It also presupposes there are well defined timing/performance requirements which isn’t always the case. If you only hit the WCET every 10000 iterations is that good enough to support the system? Can you put in a mitigation for such a situation?

Just having the value (however robustly calculated) of some resource or performance is likely to only be part of the picture.  Additionally there are cost implications in creating the models (such as processor models) in the first place which rule out their use for lower criticality systems or generic smart devices. 

My 2p…

Philippa

> 
>> - meeting other resource constraints (like stack limits)
> 
> AbsInt's StackAnalyzer can be used to do such stack analysis:
>  https://www.absint.com/stackanalyzer/index.htm <https://www.absint.com/stackanalyzer/index.htm>
> 
> Both tools are used by companies like Airbus to develop safety critical
> flight software (e.g. in A380).
> 
>> - correctness of data
> 
> At least in railway domain, tools have been developed to ensure through
> Formal Methods that data has specific properties, e.g. correct track
> topology description for CBTC (Communication Based Train Control)
> systems, as the safety of the system directly relies on the data.
> 
> RATP sells such a tool, "Ovado":
>  http://www.ovado.net/index.html <http://www.ovado.net/index.html>
> 
> ClearSy sells a similar tool.
> 
> Such tools are used by companies like Siemens or Alstom to develop their
> CBTC systems.
> 
> Sincerely yours,
> D. Mentr?
> 

Dr Philippa Ryan, Senior Consultant
Adelard LLP, 24 Waterside, 44–48 Wharf Road, London, N1 7UX
Office No: 020 7832 5850 
pmrc at adelard.com <mailto:pmrc at adelard.com> http://www.adelard.com

Registered office: Stourside Place, Station Road, Ashford, Kent TN12 1PP
Registered in England & Wales no. OC 304551. VAT no. GB 454 4898 08

This e-mail, and any attachments, is confidential and for the use of the addressee only. If you are not the intended recipient, please telephone 020 7832 5850. We do not accept legal responsibility for this e-mail or any viruses.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20171108/0e56d010/attachment-0001.html>