In: Hildesheimer Informatik-Berichte, pages 1-32. Universität Hildesheim, November 1997. Available at http://www.informatik.uni-hildesheim.de/~pep.
Abstract: In this paper a 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 addition to presenting the main ideas as well as the details of the semantics, we show that we are able to use `state of the art' verification techniques by basing our approach on M-nets (an algebra of high-level Petri nets). Therefore, we verify our running example, an ARQ (Automatic Repeat reQuest) communication protocol, using the verification component of the PEP tool which presently includes partial order based model checking and algorithms based on linear programming as well as interfaces to other verification packages such as INA, SMV and SPIN providing reduction algorithms based on BDDs, on the stubborn set or sleep set method, and on symmetries. Moreover, we give examples how the compositional nature of the M-net semantics can be used to solve the `state explosion' problem, and how interactive verification may extend the verification possibilities.
Keywords: ARQ protocol; Compositionality; Concurrency; Dynamic Processes; PEP tool; Petri Net Semantics; Procedures; SDL; Verification.