Modeling And Verification Of Queueing System With Petri Nets

Modeling, verification of system, and validation of system design are important issues of designs or developments of the complicated distributed systems.Queueing system has a deep relationship with our lives, and queueing theory is developed for researches of this systems. But queueing model is lack of the ability to analyze the system structure and the dynamic behaviors of the queueing system, and it's hard to describe the system that contains different kinds of queueing processes, and to analyze relations, restrictions and synchronizations between system components. And that is just the strength of Petri net. So, how to combine these two theories becomes the hot issue. This paper gives a feasible method.At first, this paper gives a general description of queueing theory, Petri net, generalized stochastic Petri net (GSPN), related simulating tools, and the Department of Defense Architecture Framework (DoDAF), which is related to the case study. Then, shows a mature method of queueing netwok-Petri net-layered modeling.In the principal part, this paper shows the equivalent GSPN models of kinds of essential queueing models, then, detailed describes the own method: queueing system's GSPN analyze, as well as the own Petri net simulation software developed for the method.This paper shows a case to illustrate the queueing system's GSPN analyze, and simulates it with simulation tools, then gives the result of the structure queueing analyzes. In the end, there is a compare with the layered method, followed by a conclusion of their advantages and disadvantages, as well as the solving methods and developing ways of this problem.