This paper describes an attempt to compare two toolsets allowing generation of finite labeled transition systems from underlying concurrent specification languages. The comparison is done on a specification of the leader election protocol from Home Audio/Video interoperability (HAVi) architecture. Some important semantical differences of PROMELA and $mu$CRL are identified, that lead to big differences in size of the state spaces generated for equivalent specifications.

, ,
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

Usenko, Y. (1999). A comparison of Spin and the $ mu $ CRL toolset on HAVi leader election protocol. Software Engineering [SEN]. CWI.