Formal verification of timing requirements

Question

I am aware of different formal verification tools for verifying properties of programs (The SPIN model checker for example). Are there are any common tools/methodologies for verifying timing requirements in real-time embedded systems? For example: "This algorithm must always terminate within 50 ms". How is this type of verification typically done?

Answer 1

Rate Monotonic Analysis can be useful in determining if a system is scheduleable given the activation latencies and deadlines of all the tasks. There are packages available to do the number crunching for you, but I think the math involved is not beyond a spreadsheet.

Beyond that the type of technical requirement you mentioned can be difficult to verify. Even if you have the visibility to measure the amount of time the algorithm is active, it's often impossible to test all possible scenarios to verify that the deadline is never exceeded.

What I have seen done in critical applications like pacemakers and avionics is to design the algorithm such that it will not exceed the required deadline. This can be done by either limiting the amount of data it can process in one activation, or having the function time itself and terminate early (and returning an error) if it exceeds the deadline. I hope this helps.

Answer 2

There are tool(s) UPPAAL, IF toolset for doing the model checking of timed systems. Its based on the theory of timed automata.