Verification of Estelle Specification of Distributed Systems using Coloured Petri Nets

This work is devoted to research dealing with automated constructing net models of Estelle specifications and developing verification tools of the models. We consider Estelle specifications with delay-clauses and priorities, but without dynamic constructions. The specifications allows to represent a considerable class of communication protocols. We use coloured Petri nets extended by priorities and Merlin's time concepts as the net models. This work describes a method of translating the Estelle specification into the net models, its implementation and the system NetCalc for editing and simulating the models. We present experimental results of net modeling and simulation for versions of the following well-known protocols: sliding window, ring, connection and InRes.