In: Nielsen, M.; Simpson, D.: Lecture Notes in Computer Science, Vol. 1825: 21st International Conference on Application and Theory of Petri Nets (ICATPN 2000), Aarhus, Denmark, June 2000, pages 244-260. Springer-Verlag, 2000.
Abstract: The modelling of a telecommunication protocol, ISDN-DSS1, defined using SDL, is described and the problems and methods used are discussed. The formalism used for the model is a high-level Petri net, the PROD input language which is close to a predicate/transition net. The influence of the model on the reachability analysis is also discussed with a special attention on the use of priorities and reduction methods. Finally, further development of tools which aid in modelling and analysis of this class of systems is discussed. Keywords: ISDN, DSS1, SDL, protocol verification, reachability analysis, high-level Petri nets