[SystemSafety] systemsafety Digest, Vol 63, Issue 25

[Roderick Chapman]

On 30/10/2017 11:00, systemsafety-request at lists.techfak.uni-bielefeld.de 
wrote:
> I think the discussion in this list illustrates the fact that FM (as
> normally defined) is not a panacea.
> 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.
>
> - meeting timing requirements
> - meeting other resource constraints (like stack limits)
> - correctness of data
I think you're definition of "FM" is too narrow.  OK - we go on alot
about formal verification of functional correctness of software, but
to take on two of your examples above:

For timing, we have WCET analysis (with tools from the likes of Rapita and
AbsInt), schedulability analysis, and real-time architectures like 
Time-Triggered
Architecture.

For resources, we adopt a programming style that permits static worst-case
analysis of memory, including stack usage, using tools like GNATStack.

I consider both of these to be "formal methods", just in different 
problem domains...
  - Rod