[SystemSafety] Bursting the anti formal methods bubble

[David MENTRÉ]

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/

> - 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é