Modeling Estelle specifications using colored Petri nets

Our aim is to validate distributed systems which are described by means of Estelle. This paper describes a procedure of translating the Estelle specifications into colored Petri nets extended by the priorities and Merlin’s time concepts. The considered specifications are based on standard Estelle which developed by ISO. The hierarchy specifications with time and priorities are considered. The dynamic behaviors of the Estelle specifications cannot be handled. Thus the considered subset of Estelle provides expressive power sufficient for modeling a lot of the protocols. The nets created during the translation are semisafe nets: all places except places corresponding to arrays and interaction points can contain at most one token. The translation of all constructions is described with some informal justification.