A Compositional Petri Net Semantics for SDL
Hans Fleischhack6 
and Bernd Grahlmann6
| (6) |
Fachbereich Informatik, Universität Oldenburg, Postfach 2503, D-26111 Oldenburg |
Abstract
In this paper a compositional high-level Petri net semantics for SDL (Specification and Description Language) is presented.
Emphasis is laid on the modelling of dynamic creation and termination of processes and of procedures — features, which are,
for instance, essential for typical client-server systems.
In a preliminary paper we have already shown that we are able to use ‘state of the art’ verification techniques by basing
our approach onM-nets (an algebra of high-level Petri nets). Therefore, this paper concentrates on the details of the semantics.
A distinctive feature of the presented solution is that the ‘infinite case’ (infinitely many concurrent process and procedure
instances as well as unbounded capacities of input queues and channels) is covered.
Keywords ARQ protocol - Compositionality - Concurrency - Dynamic Processes - Infinity - Petri Net Semantics - Procedures - SDL
This work has been supported by the DFG (German Research Foundation), the HCM (Human Capital and Mobility) Cooperation Network
EXPRESS, the Esprit Basic Research Working Group 6067 CALIBAN, and the Procope project POEM. It was carried out while the
second author was with the Universität Hildesheim.
References secured to subscribers.