A Compositional Proof of a Real-Time Mutual Exclusion Protocol

. 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 5 , which 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. 1 Introduction It is well--known that the major problem in applying automatic verification techniques to analyze finite--state concurrent systems is the potential combinatorial explosion of the state space arising from parallel composition. In the last few years, there has been a number of automatic verification tools for real--time systems [4, 12, 8]. Experiences with these tools show t..