university website

W.O.D. Griffioen and H.P. Korver

1995

The bakery protocol : a comparitive case-study in formal verification

Publication

Publication

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:

Additional Metadata
ACM 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)
MSC 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)
Publisher CWI
Series Department of Computer Science [CS]
Citation
Griffioen, W. O. D.& Korver, H. P. (1995). The bakery protocol : a comparitive case-study in formal verification. In Department of Computer Science [CS] (R 9569). CWI.
Free Full Text ( Final Version , 358kb ) cover


User Publication Person Organisation Collection
Close