SDL and Petri Net Performance Analysis of Communicating Systems

The automated functional and performance analysis of communicating systems specified with some Formal Description Technique has long been the goal of protocol engineers. In this paper we give 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 and performance analysis. In particular, the new type of Petri net allows one to describe the process queues and SAVE 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. We analyze the performance of a modified Inres protocol using SDL-net as the modelling paradigm. Keywords. Specification language, performance analysis, correctness analysis, Petri net, Markov process, protocol 1 Motivation The automated functional and performance analysis of communication systems specified with some Formal Description Technique has long been the goal of ..