Using simulation to test formally verified protocols ...



Title Using simulation to test formally verified protocols in complex environments
Author(s) Qiang Ye, Mike H. MacGregor
Journal Telecommunications Software Engineering: Emerging Methods, Models and Tools, Mathematical and Computer Modelling
Date 2011
Volume 53
Issue 3-4
Start page 538
End page 551
Abstract 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.
DOI 10.1016/j.mcm.2010.03.039

Using APA 6th Edition citation style.

[Page generation failure. The bibliography processor requires a browser with Javascript enabled.]

Times viewed: 442

Adding this citation to "My List" will allow you to export this citation in other styles.