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
Available as PostScript, PDF.
- ...CMC
- CMC: Compositional Model Checking