Open AccessA Compositional Proof of a Real-Time Mutual Exclusion Protocol
Author(s) -
K. Kristoffersen,
François Laroussinie,
Kim Petersén,
Paul Pettersson,
Yi Wang
Publication year - 1996
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v3i55.20058
Subject(s) - protocol (science) , mutual exclusion , correctness , state (computer science) , computer science , chemistry , mathematics , arithmetic , algorithm , theoretical computer science , medicine , alternative medicine , pathology
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.