[SystemSafety] Bursting the anti formal methods bubble

[Asier Illaro]

Hi,

For real-time multi-threaded software if you have the WCET values you could perform a Rate Monotonic Analysis. By the way, could this Rate Monotonic Analysis be considered a formal method? 

Cheers,
Asier.

-----Mensaje original-----
De: systemsafety [mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] En nombre de Peter Bishop
Enviado el: miércoles, 08 de noviembre de 2017 17:50
Para: systemsafety at lists.techfak.uni-bielefeld.de
Asunto: Re: [SystemSafety] Bursting the anti formal methods bubble

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.
_______________________________________________
The System Safety Mailing List
systemsafety at TechFak.Uni-Bielefeld.DE