Using simulation to test formally verified protocols in complex environments

Petri net modeling enables us to verify the protocol of interest formally. However, aside from formal verification, a new protocol really needs to be tested in a relatively realistic environment in which it interworks (or at least co-exists) with earlier or different versions of the same or similar protocols. Simulation excels in meeting such challenges. But the correctness of a protocol can never be proved by simulation alone. In this paper, we present an innovative methodology that combines the use of colored Petri nets and simulation (in ns-2) to obtain the advantages of deep formal verification with the broad spectrum testing of simulation. A new version of SACK TCP, α-min Paced SACK TCP, is used as the example protocol under test in our research. Our experimental results show that α-min Paced SACK TCP could reduce the number of packets queued at the bottleneck router significantly, decreasing the possibility of packet discard due to limited buffer space. Of course, the proposed methodology is a generic approach that can be used to study the performance of any new network protocol that is intended to run in an existing, complex network environment.