In: Journal of Computer and Systems Sciences, Vol. 38, No. 5, pages 771-781. 1999.
Abstract: The Estelle specifications of distributed systems with delays and priorities but without dynamic constructs are considered. For them, a method of translation into high-level Petri nets is proposed, which extend the safe colored Petri nets studied by Jensen who introduced notions of time priorities and special places representing the queues of counters. The software system intended for verifying Estelle-specified communication protocols is described, as well as the experiments in constructing network models, their simulation, and search for semantic errors.
Keywords: Estelle, Petri nets, distributed systems, system verification.