Combining Petri nets and ns-2: a hybrid method for analysis and simulation

Network protocol performance and evaluation study is often carried out using a couple of widely used simulation toolkits, such as ns-2 and OPNET. These toolkits usually contain many built-in protocol models. Using these toolkits is very efficient due to the abundant models. However, the correctness of a protocol that interests us can never be proved by simulation itself. Petri net modeling enables us to verify the protocol of interest formally. But because of the generality of Petri nets, not many network protocol models are bundled with Petri net modeling tools. In this paper we present an innovative network simulation methodology that benefits from the interaction between ns-2 and Petri nets. A communication mechanism based on Socket Programming and a synchronization mechanism used to coordinate ns-2 and Petri nets were designed to make possible the interaction. In this paper, a new version of SACK TCP, alpha-min Paced SACK TCP, is used to illustrate the power of the proposed methodology