A Correctness Proof of the Bakery Protocol in μCRL
Publication date
1992-10
Authors
Groote, J.F.
Korver, H.
Editors
Advisors
Supervisors
DOI
Document Type
Preprint
Metadata
Show full item recordCollections
License
Abstract
A specification of the bakery protocol is given in μ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 μCRL.
The proof primarily consists of algebraic manipulations based on specifications of abstract datatypes and
elementary rules and axioms from process algebra.
Keywords
Bakery Protocol, Protocol Verification, Process Algebra, Abstract Datatypes, μCRL