A practical method for reasoning about distributed systems in a theorem prover

Abstract

The Temporal Language of Transitions is the basis of a formal methodology for the verification of distributed systems. To complement modei-checking, which forms an integral part of the methodology, we contribute a proof calculus in a higher-order logic theorem prover. A method for embedding TLA[17] in the system LAMBDA is described. Motivated by the importance of practicality in an industrial setting, a simple representation of TLA is combined with extended reasoning functions. Translation of user programs, safety, liveness, and refinement proofs are depicted by way of a parametric mutual exclusion algorithm.