Verisim: formal analysis of network simulations
- 7 August 2002
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 28 (2) , 129-145
- https://doi.org/10.1109/32.988495
Abstract
Network protocols are often analyzed using simulations. We demonstrate how to extend such simulations to check propositions expressing safety properties of network event traces in an extended form of linear temporal logic. Our technique uses the INS simulator together with a component of the MaC system to provide a uniform framework. We demonstrate its effectiveness by analyzing simulations of the ad hoc on-demand distance vector (AODV) routing protocol for packet radio networks. Our analysis finds violations of significant properties and we discuss the faults that cause them. Novel aspects of our approach include modest integration costs with other simulation objectives such as performance evaluation, greatly increased flexibility in specifying properties to be checked and techniques for analyzing complex traces of alarms raised by the monitoring software.Keywords
This publication has 14 references indexed in Scilit:
- Detecting computer and network misuse through the production-based expert system toolset (P-BEST)Published by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Simulation-based 'STRESS' testing case study: a multicast routing protocolPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A flexible, extensible simulation environment for testing real-time specificationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- SCR: a toolset for specifying and analyzing requirementsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Experimental Assessment of the Period Calibration Method: A Case StudyReal-Time Systems, 1999
- Specification-based testing of reactive softwarePublished by Association for Computing Machinery (ACM) ,1997
- An automatic trace analysis tool generator for Estelle specificationsACM SIGCOMM Computer Communication Review, 1995
- Oracles for checking temporal properties of concurrent systemsPublished by Association for Computing Machinery (ACM) ,1994
- Trace analysis for conformance and arbitration testingIEEE Transactions on Software Engineering, 1989
- Defining livenessInformation Processing Letters, 1985