A Compositional Proof of a Real-Time Mutual Exclusion Protocol

Abstract

In this paper, we apply a
compositional proof technique to an automatic
verification of the correctness of
Fischer's mutual exclusion protocol. It
is demonstrated that the technique may
avoid the state-explosion problem. Our
compositional technique has recently been
implemented in a tool, CMC, which gives
experimental evidence that the size of
the verification effort required of the technique
only grows polynomially in the
size of the number of processes in the
protocol. In particular, CMC verifies the
protocol for 50 processes within 172.3
seconds and using only 32MB main memory.
In contrast all existing verification
tools for timed systems will suffer from
the state-explosion problem, and no tool
has to our knowledge succeeded in verifying
the protocol for more than 11 processes.