RCP is an industrial leader election protocol for two processes in which both timing and probablisitic aspects are crucial. It is small, easy to understand, and yet, the problems encountered in verification of this protocol are in many aspects illustrative for the application of formal methods to other real-life applications.
Several case studies, using different tools and techniques, have analysed various aspects of the protcol. This paper compares several approaches to the verification of IEEE 1394 RCP and reports on the experiences and lessons to be learned when applying formal methods to industrial applications.
Back to Workshop Programme.