In: Protocol Specification, Testing and Verification XV, pages 269-282. Chapman and Hall, 1996.
Abstract: The automated functional and performance analysis of communicating systems specified with some formal description technique has long been the goal of protocol engineers. This paper gives a description of a Petri net enhanced with queued places which enables one to automatically translate an SDL specification to a net for its direct functional ad performance analysis. In particular, the new type of Petri net allows one to describe the process queues and SVE construct, the FIFO channel queue, as well as timeouts which previously evaded temporal analysis of systems specified in SDL. The new net is called SDL-net. The performance of a modified InRes protocol is analyzed using SDL-net as the modeling paradigm.
Keywords: Markov processes, Petri nets, communication protocols, correctness analysis, performance analysis, specification languages.