Analysis and Verification of High-Level-Nets in Combination
with Formal Estelle Specifications
Jürgen Nützel, Wolfgang Fengler
E-mail: nuetzel,wfengler@theoinf.tu-ilmenau.de
Technical University of Ilmenau
Faculty for Informatics and Automation
98684 Ilmenau, Germany
This paper tries to combine the benefits of a standard specification
language like Estelle with the wide design and analysis facilities
of high-level petri nets. The formal Pascal-like language Estelle
[ISO9074] [Hogrefe89] was specially designed by ISO for the
specification of communication protocols and services. First we
present in this paper an Extended Coloured Petri Net (PN) class
which was developed for the design, verification and performance
evaluation of communication protocols. The reason for combining
Estelle with this special net class was to support the normal
Estelle designer (not knowing the profits during using petri nets)
with additional design (e.g. stochastic transitions) and simulation
features (e.g. describing the asynchronous behaviour of the
communication network).