Verisim: Verifying Network Simulations

Purpose

Verifying simulation traces of network protocols for safety properties. we use the network simulation NS along with the MaC checker to verify that the execution of a network protocol during a simulation satisfies certaing safety properties.

People

Carl Gunter, Professor
Karthikeyan Bhargavan, PhD Student
Davor Obradovic, PhD Student
Insup Lee, Professor (Collaborator)
Oleg Sokolsky, Research Associate (Collaborator
Moonjoo Kim, PhD Student (Collaborator)
Mahesh Vishwanathan, PhD Student (Collaborator)

Tools

NS, network Simulator
MaC, Run-time Checker

Status

Demonstrated the use of Verisim on AODV simulation traces. The simulation code was found to violate the safety requirements. As a result, bugs were found in the code and removed.

Papers

[1]	K. Bhargavan, C.A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, and M. Viswanathan. Verisim: Formal Analysis of Network Simulations. IEEE Transactions on Software Engineering, 28(2):129-145, February 2002. BibTeX entry Download PS. Download PDF.
[2]	Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, and Mahesh Viswanathan. Verisim: Formal analysis of network simulations International Symposium on Software Testing and Analysis, August 2000. BibTeX entry. Download PS.
[3]	Karthikeyan Bhargavan, Carl A. Gunter, and Davor Obradovic. Fault origin adjudication Formal Methods in Software Practice, August 2000. BibTeX entry. Download PS.