[SystemSafety] Bursting the anti formal methods bubble

[Peter Bishop]

As a follow-up, another real-time issue is that software has to interact
with hardware and WCET (as normally defined) does not cover the hardware
interaction time (this can be significant). A complete analysis would
require a timing/interaction model for the hardware as well as the software.
WCET analysis is also tricky for multi-threaded software designs which
have to take account of delays caused by context switching, semaphores, etc.

Peter Bishop

On 08/11/2017 10:39, Philippa Ryan wrote:
> 
> Hi,
> 
>> On 8 Nov 2017, at 07:59,
>> systemsafety-request at lists.techfak.uni-bielefeld.de
>> <mailto: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/
> 
> 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
>>
>> 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
>>
>> 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./
> 
> 
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> 

-- 

Peter Bishop
Chief Scientist
Adelard LLP
24 Waterside, 44-48 Wharf Rd, London N1 7UX
http://www.adelard.com
Recep:  +44-(0)20-7832 5850
Direct: +44-(0)20-7832 5855

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

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.