{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,6]],"date-time":"2026-01-06T13:45:26Z","timestamp":1767707126162,"version":"3.38.0"},"reference-count":73,"publisher":"SAGE Publications","issue":"11","license":[{"start":{"date-parts":[[2009,10,22]],"date-time":"2009-10-22T00:00:00Z","timestamp":1256169600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SIMULATION"],"published-print":{"date-parts":[[2010,11]]},"abstract":"<jats:p> Verification and validation (V&amp;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 \u201ccorrectness\u201d of the simulation model being used. To address this problem, we have extended J-Sim\u2014an open-source component-based network simulator written entirely in Java\u2014with 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 \u201csimilar to\u201d another in order to enable the implementation of stateful search. State ranking determines whether a state is \u201cbetter than\u201d 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. <\/jats:p>","DOI":"10.1177\/0037549709349326","type":"journal-article","created":{"date-parts":[[2009,10,23]],"date-time":"2009-10-23T00:58:51Z","timestamp":1256259531000},"page":"651-673","source":"Crossref","is-referenced-by-count":1,"title":["Assertion Checking in J-Sim Simulation Models of Network Protocols"],"prefix":"10.1177","volume":"86","author":[{"given":"Ahmed","family":"Sobeih","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana-Champaign, 201 North Goodwin Avenue, Urbana, IL 61801, USA,"}]},{"given":"Marcelo","family":"d'Amorim","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana-Champaign, 201 North Goodwin Avenue, Urbana, IL 61801, USA,"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana-Champaign, 201 North Goodwin Avenue, Urbana, IL 61801, USA,"}]},{"given":"Darko","family":"Marinov","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana-Champaign, 201 North Goodwin Avenue, Urbana, IL 61801, USA,"}]},{"given":"Jennifer C.","family":"Hou","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Illinois at Urbana-Champaign, 201 North Goodwin Avenue, Urbana, IL 61801, USA"}]}],"member":"179","published-online":{"date-parts":[[2009,10,22]]},"reference":[{"volume-title":"Discrete-event System Simulation","year":"2005","author":"Banks, J.","key":"atypb1"},{"volume-title":"Proceedings of the 2006 Winter Simulation Conference","author":"Law, A.M.","key":"atypb2"},{"volume-title":"Proceedings of the 2004 Winter Simulation Conference","author":"Balci, O.","key":"atypb3"},{"volume-title":"Proceedings of the 2003 Winter Simulation Conference","author":"Balci, O.","key":"atypb4"},{"volume-title":"Proceedings of the 2002 Winter Simulation Conference","author":"Balci, O.","key":"atypb5"},{"key":"atypb6","doi-asserted-by":"crossref","unstructured":"Balci, O. 1998. Verification, validation, and testing. The Handbook of Simulation, ed. J. Banks, John Wiley & Sons, New York, 1998, pp. 335-393.","DOI":"10.1002\/9780470172445.ch10"},{"issue":"1","key":"atypb7","first-page":"3","volume":"14","author":"Balci, O.","year":"1997","journal-title":"Transactions of the Society for Computer Simulation International"},{"volume-title":"Proceedings of the 2005 Winter Simulation Conference","author":"Sargent, R.G.","key":"atypb8"},{"key":"atypb9","unstructured":"J-Sim. http:\/\/www.j-sim.org\/ ."},{"volume-title":"Physical implementation of ad hoc network routing protocols using unmodified ns-2 models","year":"2004","author":"Saha, A.K.","key":"atypb10"},{"key":"atypb11","first-page":"99","author":"Perkins, C.E.","year":"1999","journal-title":"Proceedings of IEEE WMCSA\u2019"},{"journal-title":"IETF Draft","year":"2002","author":"Perkins, C.","key":"atypb12"},{"key":"atypb13","volume":"3561","author":"Perkins, C.","year":"2003","journal-title":"Request for Comments"},{"key":"atypb14","first-page":"04","author":"Sobeih, A.","year":"2004","journal-title":"Proceedings of ACM-IEEE MEMOCODE\u2019"},{"key":"atypb15","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_17"},{"volume-title":"Verification of Simulation Models of Network Protocols Using State Space Exploration. PhD thesis, Department of Computer Science","year":"2008","author":"Sobeih, A.","key":"atypb16"},{"volume-title":"Java PathFinder (JPF)","key":"atypb17"},{"journal-title":"Proceedings of IEEE ASE\u2019","first-page":"00","author":"Visser, W.","key":"atypb18"},{"volume-title":"Model Checking","year":"1999","author":"Clarke, E.M.","key":"atypb19"},{"volume-title":"Design, Realization and Evaluation of a Component-based Compositional Software Architecture for Network Simulation. PhD thesis","year":"2002","author":"Tyan, H.-Y.","key":"atypb20"},{"volume-title":"Communication and Concurrency","year":"1989","author":"Milner, R.","key":"atypb21"},{"key":"atypb22","first-page":"06","author":"Dwyer, M.B.","year":"2006","journal-title":"Proceedings of ACM FSE\u2019"},{"journal-title":"Proceedings of ICSE\u2019","first-page":"07","author":"Dwyer, M.B.","key":"atypb23"},{"volume-title":"The Art of Computer Programming, volume 2: Seminumerical Algorithms","year":"1998","author":"Knuth, D.E.","key":"atypb24"},{"key":"atypb25","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"atypb26","first-page":"02","author":"Musuvathi, M.","year":"2002","journal-title":"Proceedings of OSDI\u2019"},{"volume-title":"Proceedings of the IEEE International Conference on Automated Software Engineering","author":"Iosif, R.","key":"atypb27"},{"volume-title":"Java Native Interface: Programmer\u2019s Guide and Specification","key":"atypb28"},{"key":"atypb29","first-page":"04","author":"Visser, W.","year":"2004","journal-title":"Proceedings of ACM ISSTA\u2019"},{"key":"atypb30","first-page":"05","author":"Visser, W.","year":"2005","journal-title":"Proceedings of IEEE\/ACM ASE\u2019"},{"key":"atypb31","first-page":"06","author":"Visser, W.","year":"2006","journal-title":"Proceedings of ACM ISSTA\u2019"},{"key":"atypb32","doi-asserted-by":"publisher","DOI":"10.1080\/01966324.1984.10737151"},{"key":"atypb33","first-page":"04","author":"Musuvathi, M.","year":"2004","journal-title":"Proceedings of NSDI\u2019"},{"key":"atypb34","first-page":"97","author":"Godefroid, P.","year":"1997","journal-title":"Proceedings of ACM POPL\u2019"},{"key":"atypb35","first-page":"05","author":"Flanagan, C.","year":"2005","journal-title":"Proceedings of ACM POPL\u2019"},{"key":"atypb36","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0104-3"},{"key":"atypb37","first-page":"02","author":"Godefroid, P.","year":"2002","journal-title":"Proceedings of TACAS\u2019"},{"key":"atypb38","doi-asserted-by":"publisher","DOI":"10.1145\/1029894.1029922"},{"journal-title":"Proceedings of ACM\/IEE DAC\u2019 98","year":"1998","author":"Yang, C.H.","key":"atypb39"},{"key":"atypb40","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0130-9"},{"journal-title":"Proceedings of IEEE IPDPS 2007, NSF Next Generation Software Program Workshop","year":"2007","author":"Sobeih, A.","key":"atypb41"},{"key":"atypb42","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"atypb43","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"volume-title":"Symbolic Analysis Laboratory","key":"atypb44"},{"journal-title":"Proceedings of IEEE ICCD\u2019","first-page":"92","author":"Dill, D.L.","key":"atypb45"},{"volume-title":"Proceedings of the 2003 Winter Simulation Conference","author":"Rue\u00df, H.","key":"atypb46"},{"key":"atypb47","first-page":"00","author":"Park, D.Y.W.","year":"2000","journal-title":"Proceedings of IEEE ASE\u2019"},{"journal-title":"Proceedings of SPIN\u2019","first-page":"99","author":"Havelund, K.","key":"atypb48"},{"key":"atypb49","first-page":"00","author":"Corbett, J.","year":"2000","journal-title":"Proceedings of ICSE\u2019"},{"key":"atypb50","first-page":"04","author":"Farzan, A.","year":"2004","journal-title":"Proceedings of CAV\u2019"},{"key":"atypb51","doi-asserted-by":"publisher","DOI":"10.1109\/32.988495"},{"volume-title":"The Network Simulator-ns-2","key":"atypb52"},{"journal-title":"Proceedings of ECRTS\u2019","first-page":"99","author":"Kim, M.","key":"atypb53"},{"key":"atypb54","volume-title":"Theory of Modeling and Simulation","author":"Zeigler, B.P.","year":"2000","edition":"2"},{"journal-title":"International Series in Computer Science","year":"1992","author":"Spivey, M.","key":"atypb55"},{"volume-title":"Proceedings of the 2006 Winter Simulation Conference","author":"Traore, M.K.","key":"atypb56"},{"volume-title":"ZUM \u201997: Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation","author":"Saaltink, M.","key":"atypb57"},{"volume-title":"Proceedings of the 2006 Winter Simulation Conference","author":"Martens, J.","key":"atypb58"},{"key":"atypb59","doi-asserted-by":"publisher","DOI":"10.1145\/1176249.1176253"},{"key":"atypb60","first-page":"98","author":"Bernardo, M.","year":"1998","journal-title":"Proceedings of IFIP FORTE\/PSTV\u2019"},{"volume-title":"Maude","key":"atypb61"},{"volume-title":"Maude 2.3 manual","year":"2007","author":"Clavel, M.","key":"atypb62"},{"key":"atypb63","first-page":"97","author":"Bernardo, M.","year":"1997","journal-title":"Proceedings of ICALP\u2019"},{"key":"atypb64","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00127-8"},{"journal-title":"Proceedings of CAV\u2019","first-page":"96","author":"Cleaveland, R.","key":"atypb65"},{"volume-title":"Introduction to the Numerical Solution of Markov Chains","year":"1994","author":"Stewart, W.J.","key":"atypb66"},{"key":"atypb67","doi-asserted-by":"publisher","DOI":"10.1145\/379525.379526"},{"key":"atypb68","first-page":"02","author":"Eker, S.","year":"2002","journal-title":"Proceedings of WRLA\u2019"},{"key":"atypb69","first-page":"04","author":"\u00d6lveczky, P.","year":"2004","journal-title":"Proceedings of FASE\u2019"},{"key":"atypb70","first-page":"01","author":"\u00d6lveczky, P.","year":"2001","journal-title":"Proceedings of FASE\u2019"},{"key":"atypb71","doi-asserted-by":"publisher","DOI":"10.1109\/65.819171"},{"key":"atypb72","first-page":"06","author":"\u00d6lveczky, P.","year":"2006","journal-title":"Proceedings of International Workshop on Parallel and Distributed Real-Time Systems 2006, held in conjunction with IEEE IPDPS\u2019"},{"issue":"1","key":"atypb73","first-page":"89","volume":"1","author":"Zhang, H.","year":"2005","journal-title":"Wireless Ad Hoc and Sensor Networks: An International Journal"}],"container-title":["SIMULATION"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0037549709349326","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0037549709349326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T10:29:16Z","timestamp":1740911356000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/0037549709349326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,10,22]]},"references-count":73,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2010,11]]}},"alternative-id":["10.1177\/0037549709349326"],"URL":"https:\/\/doi.org\/10.1177\/0037549709349326","relation":{},"ISSN":["0037-5497","1741-3133"],"issn-type":[{"type":"print","value":"0037-5497"},{"type":"electronic","value":"1741-3133"}],"subject":[],"published":{"date-parts":[[2009,10,22]]}}}