[SystemSafety] Bursting the anti formal methods bubble

[Peter Bishop]

On 07/11/2017 11:36, David MENTRÉ wrote:
> 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.

Indeed - I did include the caveat "(as normally defined)"

The resource usage tools mentioned analyse code at a different level
(e.g. binary code) - though unfortunately not for the processors I run
across in my work.
While not formal in the conventional sense, they do address some key
properties of real-time systems

I was not familiar with the data correctness tools
- looks like a useful advance in the application of formal methods.

rgds

Peter

> 
>> - meeting timing requirements
> 
> AbsInt's aiT WCET Analyzers can be used to do such WCET analysis using FM:
> 
>   https://www.absint.com/ait/
> 
>> - 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é
> 
> _______________________________________________
> 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.