A Compositional Proof of a Real-Time Mutual Exclusion Protocol

Kåre J. Kristoffersen, Francois Laroussinie, Kim G. Petersen, Paul Pettersson, Wang Yi


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.

Full Text:


DOI: http://dx.doi.org/10.7146/brics.v3i55.20058
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library