A comparison of Spin and the $ mu $ CRL toolset on HAVi leader election protocol
Yaroslav S. Usenko · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1999
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 di#erences of PROMELA and CRL are identified, that lead to big di#erences in size of the state spaces generated for equivalent specifications. 1991 Mathematics Subject Classification: 68Q22; 68Q45; 68Q60 1991 ACM Computing Classification System: D.1.3; D.2.4; D.2.8 Keywords and Phrases: CRL, SPIN, Tool Comparison, State Space Generation, Specification, Deadlock Checking. Note: Work carried out under project SEN 2.1 Process Specification and Analysis. 1. Introduction With current state of the art in software verification a lot of the analysis methods are based on finite labeled transition systems (FLTS). There is a number of tools to manipulate with them, to check...