[SystemSafety] Bursting the anti formal methods bubble

[Matthew Squair]

Throw in that digital is just analog driven to the extreme, plus aging
component effects and voila, the Byzantine generals are on the march again.
:)

On 11 November 2017 at 2:51:17 am, Derek M Jones (derek at knosof.co.uk) wrote:

> 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
> _______________________________________________
> 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/a4d80e9c/attachment-0001.html>