AbstractAbstract This paper presents a Petri net model, called the interpreted coloured Petri net, which allows the verification of parallel systems specified with the ISO language Estelle. The main contribution of this model is to take into account parallel behaviours with strong synchronism constraints. Such behaviours are often encountered in real-time systems in which parallel execution is controlled by a clock tip. Our model allows the expression of simultaneous executions as it can be specified in Estelle. Moreover, this model is the basis of a protocol verification tool called Petristelle.