Verification and validation (V&V) is a critically important phase in the development life cycle of a simulation model. In the context of network simulation, traditional network simulators perform well in using a simulation model for evaluating the performance of a network protocol but lack the capability to check the “correctness” of the simulation model being used. To address this problem, we have extended J-Sim—an open-source component-based network simulator written entirely in Java—with a state space exploration (SSE) capability that explores the state space created by a network simulation model, up to a configurable maximum depth, in order to find an execution (if any) that violates an assertion, i.e. a property specifying an invariant that must always hold true in all states. In this paper, we elaborate on the SSE framework in J-Sim and present one of our fairly complex case studies, namely verifying the simulation model of the Ad-hoc On-demand Distance Vector (AODV) routing protocol for wireless ad-hoc networks. The SSE framework makes use of protocol-specific properties along two orthogonal dimensions: state similarity and state ranking. State similarity determines whether a state is “similar to” another in order to enable the implementation of stateful search. State ranking determines whether a state is “better than” another in order to enable the implementation of best-first search (BeFS). Specifically, we develop protocol-specific search heuristics to guide SSE towards finding assertion violations in less time. We evaluate the efficiency of our SSE framework by comparing its performance with that of a state-of-the-art model checker for Java programs, namely Java PathFinder (JPF). The results of the comparison show that the time needed to find an assertion violation by our SSE framework in J-Sim can be significantly less than that in JPF unless a substantial amount of programming effort is spent in JPF to make its performance close to that of our SSE framework.
Banks, J., J.S. Carson II, B.L. Nelson and D.M. Nicol.2005. Discrete-event System Simulation. Prentice-Hall, Englewood Cliffs, NJ, 2005.
2.
Law, A.M.2006. How to build valid and credible simulation models. Proceedings of the 2006 Winter Simulation Conference.
3.
Balci, O.2004. Quality assessment, verification, and validation of modeling and simulation applications. Proceedings of the 2004 Winter Simulation Conference.
4.
Balci, O.2003. Verification, validation, and certification of modeling and simulation applications. Proceedings of the 2003 Winter Simulation Conference.
5.
Balci, O., R.E. Nance, J.D. Arthur and W.F. Ormsby.2002. Expanding our horizons in verification, validation, and accreditation research and practice. Proceedings of the 2002 Winter Simulation Conference.
6.
Balci, O.1998. Verification, validation, and testing. The Handbook of Simulation, ed. J. Banks, John Wiley & Sons, New York, 1998, pp. 335-393.
7.
Balci, O.1997. Principles of simulation model validation, verification, and testing. Transactions of the Society for Computer Simulation International, 14(1):3-12.
8.
Sargent, R.G.2005. Verification and validation of simulation models. Proceedings of the 2005 Winter Simulation Conference.
9.
J-Sim.http://www.j-sim.org/ .
10.
Saha, A.K., K. To, S. PalChaudhuri, S. Du and D.B. Johnson.2004. Physical implementation of ad hoc network routing protocols using unmodified ns-2 models. In ACM MobiCom’04. Poster .
11.
Perkins, C.E. and E.M. Royer.1999. Ad-hoc on-demand distance vector routing. Proceedings of IEEE WMCSA’99.
12.
Perkins, C., E. Royer and S. Das .2002. Ad hoc On-demand Distance Vector (AODV) routing. IETF Draft , January 2002.
13.
Perkins, C., E. Royer and S. Das .2003. Ad hoc On-demand Distance Vector (AODV) routing. Request for Comments3561, July 2003.
14.
Sobeih, A. , M. Viswanathan and J.C. Hou.2004. Check and Simulate: A case for incorporating model checking in network simulation . Proceedings of ACM-IEEE MEMOCODE’04.
15.
Sobeih, A. , M. Viswanathan, D. Marinov, and J.C. Hou .2005. Finding bugs in network protocols using simulation code and protocol-specific heuristics. Proceedings of ICFEM’05 (Lecture Notes in Computer Science, vol. 3785), Springer, Berlin .
16.
Sobeih, A.2008. Verification of Simulation Models of Network Protocols Using State Space Exploration. PhD thesis, Department of Computer Science , University of Illinois at Urbana-Champaign.
Visser, W. , K. Havelund, G. Brat and S. Park.Model checking programs. Proceedings of IEEE ASE’00.
19.
Clarke, E.M. , O. Grumberg and D. Peled.1999. Model Checking. MIT Press, Cambridge, MA.
20.
Tyan, H.-Y.2002. Design, Realization and Evaluation of a Component-based Compositional Software Architecture for Network Simulation. PhD thesis, Department of Electrical Engineering, The Ohio State University.
21.
Milner, R.1989. Communication and Concurrency. Prentice-Hall , Englewood Cliffs, NJ.
22.
Dwyer, M.B. , S. Person and S. Elbaum.2006. Controlling factors in evaluating path-sensitive error detection techniques . Proceedings of ACM FSE’06.
23.
Dwyer, M.B. , S. Elbaum, S. Person and R. Purandare.Parallel randomized state-space search . Proceedings of ICSE’07.
24.
Knuth, D.E.1998. The Art of Computer Programming, volume 2: Seminumerical Algorithms. Addison-Wesley, Reading, MA.
25.
Bhargavan, K. , D. Obradovic, and C.A. Gunter.2002. Formal verification of standards for distance vector routing protocols . Journal of the ACM, 49(4):538-576.
26.
Musuvathi, M. , D.Y.W. Park, A. Chou, D.R. Engler and D.L. Dill.2002. CMC: A pragmatic approach to model checking real code. Proceedings of OSDI’02.
27.
Iosif, R.2002. Exploiting heap symmetries in explicit-state model checking of software. Proceedings of the IEEE International Conference on Automated Software Engineering (ASE 2001).
28.
Java Native Interface: Programmer’s Guide and Specification . http://java.sun.com/docs/books/jni/.
29.
Visser, W., C.S. Pasareanu, and S. Khurshid.2004. Test input generation with Java PathFinder . Proceedings of ACM ISSTA’04.
30.
Visser, W., C.S. Pasareanu and R. Pelanek.2005. Test input generation for red-black trees using abstraction . In Proceedings of IEEE/ACM ASE’05.
31.
Visser, W. , C.S. Pasareanu, and R. Pelanek.2006. Test input generation for Java containers using state matching. Proceedings of ACM ISSTA’06.
32.
Balci, O. and R.G. Sargent.1984. Validation of simulation models via simultaneous confidence intervals. American Journal of Mathematical and Management Sciences, 4(3-4):375-406.
33.
Musuvathi, M. and D.R. Engler.2004. Model checking large network protocol implementations. Proceedings of NSDI’04.
34.
Godefroid, P.1997. Model checking for programming languages using VeriSoft. Proceedings of ACM POPL’97.
35.
Flanagan, C. and P. Godefroid.2005. Dynamic partial-order reduction for model checking software. Proceedings of ACM POPL’05.
36.
Edelkamp, S., S. Leue and A. Lluch-Lafuente.2004. Directed explicit-state model checking in the validation of communication protocols. International Journal on Software Tools for Technology Transfer (STTT), 5(2-3):247-267.
37.
Godefroid, P. and S. Khurshid.2002. Exploring very large state spaces using genetic algorithms. Proceedings of TACAS’02.
38.
Tan, J., G.S. Avrunin, L.A. Clarke, S. Zilberstein and S. Leue.2004. Heuristic-guided counterexample search in FLAVERS. Proceedings of ACM SIGSOFT’ 04/FSE-12.
39.
Yang, C.H. and D.L. Dill.1998. Validation with guided search of the state space. Proceedings of ACM/IEE DAC’ 98.
40.
Groce, A. and W. Visser.2004. Heuristics for model checking Java programs. International Journal on Software Tools for Technology Transfer (STTT), 6(4):260-276.
41.
Sobeih, A. , M. Viswanathan, D. Marinov and J.C. Hou .2007. J-Sim: An integrated environment for simulation and model checking of network protocols. Proceedings of IEEE IPDPS 2007, NSF Next Generation Software Program Workshop.
42.
Holzmann, G.J.1997. The model checker SPIN . IEEE Transactions on Software Engineering, 23(5):279-295.
43.
McMillan, K.1993. Symbolic Model Checking . Kluwer Academic , Dordrecht.
Dill, D.L. , A.J. Drexler, A.J. Hu and C.H. Yang.Protocol verification as a hardware design aid. Proceedings of IEEE ICCD’92.
46.
Rueß, H. and L. de Moura .2003. From simulation to verification (and back). Proceedings of the 2003 Winter Simulation Conference.
47.
Park, D.Y.W. , U. Stern, J.U. Skakkebæk and D.L. Dill.2000. Java model checking. Proceedings of IEEE ASE’00.
48.
Havelund, K.Java PathFinder, A translator from Java to Promela. Proceedings of SPIN’99.
49.
Corbett, J., M.B. Dwyer, J. Hatcliff, S. Laubach, C.R. Păsăreanu and H. Zheng.2000. Bandera: Extracting finite state models from Java source code. Proceedings of ICSE’00.
50.
Farzan, A. , Chen, F., J. Meseguer and G. Rosu.2004. Formal analysis of Java programs in JavaFAN. Proceedings of CAV’04.
51.
Bhargavan, K., C.A. Gunter, M. Kim , I. Lee , D. Obradovic, O. Sokolsky and M. Viswanathan.2002. Verisim: Formal analysis of network simulations. IEEE Transactions on Software Engineering, 28(2):129-145.
52.
The Network Simulator-ns-2. http://www.isi.edu/nsnam/ns/ .
53.
Kim, M., M. Viswanathan, H. Ben-Abdallah, S. Kannan, I. Lee and O. Sokolsky.Formally specified monitoring of temporal properties. Proceedings of ECRTS’99.
54.
Zeigler, B.P. , T.G. Kim and H. Praehofer.2000. Theory of Modeling and Simulation. 2nd edition, Academic Press, New York.
55.
Spivey, M.1992. The Z Notation: A Reference Manual. (International Series in Computer Science), Prentice-Hall, Englewood Cliffs, NJ.
56.
Traore, M.K.2006. Analyzing static and temporal properties of simulation models. Proceedings of the 2006 Winter Simulation Conference.
57.
Saaltink, M.1997. The Z/EVES system. ZUM ’97: Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation, 1997.
58.
Martens, J. , K. Pauwels and F. Put .2006. A neural network approach to the validation of simulation models. Proceedings of the 2006 Winter Simulation Conference.
59.
Martens, J., F. Put and E. Kerre.2006. A fuzzy set theoretic approach to validate simulation models. ACM Transactions on Modeling and Computer Simulation, 16(4):375-398.
60.
Bernardo, M., W.R. Cleaveland, S.T. Sims and W.J. Stewart.1998. TwoTowers: A tool integrating functional and performance analysis of concurrent systems. Proceedings of IFIP FORTE/PSTV’98.
61.
Maude. http://maude.cs.uiuc.edu.
62.
Clavel, M., F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer and C. Talcott.Maude 2.3 manual, January 2007.
63.
Bernardo, M.1997. An algebra-based method to associate rewards with EMPA terms. Proceedings of ICALP’97.
64.
Bernardo, M. and R. Gorrieri.1998. A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoretical Computer Science, 202:1-54.
65.
Cleaveland, R. and S. Sims.The NCSU concurrency workbench . Proceedings of CAV’96.
66.
Stewart, W.J.1994. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton, NJ.
67.
Aldini, A. , R. Gorrieri, M. Roccetti and M. Bernardo.2001. Comparing the QoS of Internet audio mechanisms via formal methods. ACM Transactions on Modeling and Computer Simulation, 11(1):1-42.
68.
Eker, S., J. Meseguer and A. Sridharanarayanan.2002. The Maude LTL model checker. Proceedings of WRLA’02.
69.
Ölveczky, P. and J. Meseguer.2004. Specification and analysis of real-time systems using Real-Time Maude. Proceedings of FASE’04.
70.
Ölveczky, P., M. Keaton, J. Meseguer, C. Talcott and S. Zabele.2001. Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. Proceedings of FASE’01.
71.
Kasera, S.K. , S. Bhattacharyya, M. Keaton, D. Kiwior, S. Zabele, J. Kurose and D. Towsley.2000. Scalable fair reliable multicast using active services. IEEE Network Magazine, 14(1):48-57.
72.
Ölveczky, P. and S. Thorvaldsen.2006. Formal modeling and analysis of wireless sensor network algorithms in Real-Time Maude . Proceedings of International Workshop on Parallel and Distributed Real-Time Systems 2006, held in conjunction with IEEE IPDPS’06.
73.
Zhang, H. and J.C. Hou .2005. Maintaining sensing coverage and connectivity in large sensor networks. Wireless Ad Hoc and Sensor Networks: An International Journal, 1(1-2):89-123.
