A correctness proof of the bakery protocol in $ mu $CRL
A specification of a bakery protocol is given in $mu$CRL. We provide a simple correctness criterion for the protocol. Then the protocol is proven correct using a proof system that has been developed for $mu$CRL. The proof primarily consists of algebraic manipulations based on specifications of abstract data types and elementary rules and axioms from process algebra.
|Department of Computer Science [CS]|
|Organisation||Computer Systems & Telematics|
Groote, J.F, & Korver, H.P. (1994). A correctness proof of the bakery protocol in $ mu $CRL. Department of Computer Science [CS]. CWI.