A Compositional Proof of a Real-Time Mutual Exclusion Protocol

Publisher Website
Google Scholar
Abstract
In this paper, we apply acompositional proof technique to an automaticverification of the correctness ofFischer's mutual exclusion protocol. Itis demonstrated that the technique mayavoid the state-explosion problem. Ourcompositional technique has recently beenimplemented in a tool, CMC, which givesexperimental evidence that the size ofthe verification effort required of the techniqueonly grows polynomially in thesize of the number of processes in theprotocol. In particular, CMC verifies theprotocol for 50 processes within 172.3seconds and using only 32MB main memory.In contrast all existing verificationtools for timed systems will suffer fromthe state-explosion problem, and no toolhas to our knowledge succeeded in verifyingthe protocol for more than 11 processes.

This publication has 0 references indexed in Scilit: