This Article 
 Bibliographic References 
 Add to: 
Verisim: Formal Analysis of Network Simulations
February 2002 (vol. 28 no. 2)
pp. 129-145

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 NS 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.

[1] B. Alpern and F.B. Schneider, “Defining Liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181-185, Oct. 1985.
[2] D. Anderson, T. Frivold, and A. Valdes, “Next-Generation Intrusion Detection Expert System (NIDES): A Summary,” Technical Report, SRI-CSL-95-07, May 1995.
[3] K. Bhargavan, C.A. Gunter, and D. Obradovic, “An Assessment of Tools Used in the Verinet Project,” Technical Report MS-CIS-00-15, Univ. of Pennsylvania, 2000, .
[4] K. Bhargavan, C.A. Gunter, and D. Obradovic, “A Taxonomy of Logical Network Analysis Techniques,” Technical Report MS-CIS-00-14, Univ. of Pennsylvania, 2000, .
[5] K. Bhargavan, D. Obradovic, and C.A. Gunter, “Formal Verification of Standards for Distance Vector Routing Protocols,” Feb. 2000, .
[6] G.V. Bochmann and O. Bellal, “Test Result Analysis with Respect to Formal Specifications,” Proc. Second Int'l Workshop Protocol Test Systems, pp. 272-294, Oct. 1989.
[7] G.V. Bochmann, D. Desbiens, M. Dubuc, D. Ouimet, and F. Saba, “Test Result Analysis and Validation of Test Verdicts,” Proc. Workshop Protocol Test Systems (IFIP), 1990.
[8] G. v. Bochmann, R. Dssouli, and J. Zhao, "Trace Analysis for Conformance and Arbitration Testing," IEEE Trans. Software. Eng., vol. 15, no. 11, pp. 1,347-1,356, Nov. 1989.
[9] J. Broch, D.A. Maltz, D.B. Johnson, Y.C. Hu, and J. Jetcheva, “A Performance Comparison of Multi-Hop Wireless Ad Hoc Network Routing Protocols,” Proc. Conf. Mobile Computing MOBICOM, pp. 85-97, 1998.
[10] M. Brockmeyer, F. Jahanian, C. Heitmeyer, and B. Labaw, “A Flexible, Extensible Environment for Testing Real-Time Specifications,” Proc. IEEE Real-Time Technology and Applications Symp. (RTAS), 1997.
[11] L.K. Dillon and Q. Yu, “Oracles for Checking Temporal Properties of Concurrent Systems,” Proc. Symp. Foundations of Software Eng., pp. 140–153, Dec. 1994.
[12] S.A. Ezust and G.V. Bochmann, “An Automatic Trace Analysis Tool Generator for Estelle Specifications,” Computer Comm. Rev., Proc. ACM SIGCOMM '95 Conf., vol. 25, no. 4, pp. 175-184, Oct. 1995.
[13] K. Fall and K. Varadhan, “The VINT Project,” ns Notes and Documentation, Feb. 2000.
[14] C.L. Heitmeyer, A. Bull, C. Gasarch, and B.G. Labaw, “SCR*: A Toolset for Specifying and Analyzing Requirements,” Proc. Conf. Computer Assurance (COMPASS), pp. 109–122, June 1995.
[15] A. Helmy and D. Estrin, "Simulation-Based 'STRESS' Testing Case Study: A Multicast Routing Protocol," Proc. Int'l Symp. Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, IEEE CS Press, Los Alamitos, Calif., 1998, pp. 36-43.
[16] L.J. Jagadeesan, A. Porter, C. Puchol, J.C. Ramming, and L.G. Votta, “Specification-Based Testing of Reactive Software: Tools and Experiments,” Proc. Int'l Conf. Software Eng., May 1997.
[17] M. Kim, M. Viswanathan, H. Ben-Abdallah, S. Kannan, I. Lee, and O. Sokolsky, “Formally Specified Monitoring of Temporal Properties,” Proc. European Conf. Real-Time Systems, 1999.
[18] I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan, “Runtime Assurance Based on Formal Specifications,” Proc. Int'l Conf. Parallel and Distributed Processing Techniques and Applications, 1999.
[19] U. Lindqvist and P.A. Porras, “Detecting Computer and Network Misuse Through the Production-Based Expert System Toolset (P-BEST),” Proc. 1999 IEEE Symp. Security and Privacy, May 1999.
[20] T.O. O'Malley, D.J. Richardson, and L.K. Dillon, “Efficient Specification-Based Test Oracles,” Proc. Second California Software Symp. (CSS '96), Apr. 1996.
[21] C. Perkins, “Ad Hoc On-Demand Distance Vector (AODV) Routing,” Internet-Draft Version 00, (IETF), Nov. 1997.
[22] C. Perkins and E. Royer, Ad Hoc on Demand Distance Vector (AODV) Routing Proc. Second IEEE Workshop Mobile Computing Systems and Applications, pp. 90-100, Feb. 1999.
[23] P.A. Porras and P.G. Neumann, “EMERALD: Event Monitoring Enabling Responses to Anomalous Live Disturbances,” Proc. Nat'l Information Systems Security Conf., 1997.
[24] D.J. Richardson, S.L. Aha, and T.O. O'Malley, “Specification-Based Oracles for Reactive Systems,” Proc. 14th Int'l Conf. Software Eng., May 1992.
[25] M. Viswanathan, “Foundations for the Run-Time Analysis of Software Systems,” PhD thesis, Univ. of Pennsylvania, Philadelphia, Dec. 2000.

Index Terms:
Verisim, formal analysis, network, simulation, testing, routing, NS, MaC, AODV, temporal logic, ad hoc networks,packet radio, tuning, population abstraction, packet-type abstraction.
K. Bhargavan, C.A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, M. Viswanathan, "Verisim: Formal Analysis of Network Simulations," IEEE Transactions on Software Engineering, vol. 28, no. 2, pp. 129-145, Feb. 2002, doi:10.1109/32.988495
Usage of this product signifies your acceptance of the Terms of Use.