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 for Distributed Systems and Communications Protocols,Chapman and Hall, 1994, pages 259-273.

Berne, Switzerland, October 4-7, 1994,

Abstract

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.