An Estelle-NPN based system for protocol verification

Estelle is one of the formal description techniques developed by ISO for specifying distributed and concurrent information processing systems. Verification of Estelle specifications is still the subject of much research. We have developed an approach to verifying standard Estelle specifications by translating them into numerical Petri net (NPN) specifications. The merits of this approach are that all dynamic behaviours, exported variables and most Estelle statements can be handled. The deficiencies are that priority and delay clauses and the system process attribute can not be modelled. In this paper, we present a set of tools using this approach for the automatic verification of protocols specified in Estelle. The verification of the sliding-window protocol is used to demonstrate the usefulness of this set of tools