“Verifying timing properties of concurrent algorithms”

Victor Luchangco, Ekrem Söylemez, Stephen Garland, and Nancy Lynch

FORTE '94: Seventh International Conference on Formal Description Techniques, pages 259–273, Berne, Switzerland, October 4–7, 1994. Chapman & Hall.

This paper presents a method for computer-aided verification 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.

Back to Publications of Stephen J. Garland