Proving Performance Properties (even Probabilistic Ones)

Abstract: This paper surveys some new tools and methods for formally verifying time performance properties of systems that satisfy timing assumptions. The techniques are potentially of practical benet in the validation of real-time process control and communication systems. The tools and methods include nondeterministic timed automaton models, invariant assertion and simulation techniques for proving worst-case time bounds, probabilistic timed automaton models, and Markov-style techniques for proving probabilistic time bounds. All of these techniques are well suited for (partial) mechanization.