[SystemSafety] Bursting the anti formal methods bubble

Derek M Jones derek at knosof.co.uk
Fri Nov 10 16:51:17 CET 2017


Todd,

> 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

It's any processor whose basic components are built from a handful of
atoms.  Variations in manufacturing mean that an atom difference here
and there can now have a significant impact on performance.

Your cpus may all start clocking at 1 GHz, but atom differences mean
their power characteristics are slightly different, some will heat up
faster than others; get too hot and the temperature management will
reduce the clock rate to cool things down.  Now you have the 'same'
processors running identical code at different speeds.

Some data and pictures here:
http://shape-of-code.coding-guidelines.com/2015/02/24/hardware-variability-may-be-greater-than-algorithmic-improvement/

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

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com


More information about the systemsafety mailing list