Verifying timing properties of concurrent algorithms.

Abstract

This paper presents a method for computer-aided veri cation of timing properties of real-time systems. A timed automaton model, along with invariant assertion and simulation techniques for proving properties of real-time systems, is formalized within the Larch Shared Language. This framework is then used to prove time bounds for two sample algorithms|a simple counter and Fischer's mutual exclusion protocol. The proofs are checked using the Larch Prover.