[SystemSafety] Bursting the anti formal methods bubble

[Todd Carpenter]

> For real-time multi-threaded software if you have the WCET
> values you could perform a Rate Monotonic Analysis.

Only if the underlying scheduler is RMA. However, RMA may not satisfy
your needs to support different processing rates, response time
requirements, jitter requirements, and communications strategies in a
distributed system. RMA is also not confidentally secure: it supports
signaling between rates. RMA also does not work for hierarchical
scheduling (e.g., multiple separate real time partitions running on a
hypervisor).

> By the way, could this Rate Monotonic Analysis be considered a
> formal method?

Yes, subject to RMA satisfying your application requirements. If your
problem is simple enough, or can be sufficiently constrained, sure.

As an aside, good luck getting meaningful WCET numbers on a modern Intel
processor, unless your problem is simple enough (e.g., no core or cache
interactions). Intel keeps all sorts of caches behind the scenes, and
you can't clear them. ARM real-time cores are better for this sort of
thing, but you still have to be very careful about the cache
interactions. But yes, I'll conceded the point, "if you have good WCET
values, then you can do X."


On 11/10/2017 5:16 AM, Asier Illaro wrote:
> 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
>>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20171110/5afea543/attachment.html>