State space generation for the HAVi leader election protocol

This paper describes two specifications of the leader election protocol from the home audio/video interoperability (HAVi) architecture. The specifications were written in two concurrent specification languages: μCRL and PROMELA. Two toolsets allowing generation of finite labeled transition systems, for μCRL and PROMELA, respectively, were applied in this case study. The results of the state space generation by both tools and some conclusions on the semantical differences between PROMELA and μCRL are presented in this paper.