The bakery protocol : a comparitive case-study in formal verification
A Comparative Case-Study in Formal Verification Groote and the second author verified (a version of) the Bakery Protocol in $muCRL$. Their process-algebraic verification is rather complex compared to the protocol. Now the question is: How do other verification techniques perform on this protocol? In this paper, we present a new correctness proof by using I/O-automata theory and discuss the relative merits of both approaches. Subject classification:
|Software/Program Verification (acm D.2.4), Models of Computation (acm F.1.1), Specifying and Verifying and Reasoning about Programs (acm F.3.1), Mathematical Logic (acm F.4.1)|
|Classical first-order logic (msc 03B10), Grammars and rewriting systems (msc 68Q42), Theory of computing (msc 68Qxx), Specification and verification (program logics, model checking, etc.) (msc 68Q60), Abstract data types; algebraic specification (msc 68Q65)|
|Department of Computer Science [CS]|
Griffioen, W.O.D, & Korver, H.P. (1995). The bakery protocol : a comparitive case-study in formal verification. Department of Computer Science [CS]. CWI.