{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T13:42:56Z","timestamp":1777902176074,"version":"3.51.4"},"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,22]],"date-time":"2009-10-22T20:58:51Z","timestamp":1256245131000},"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,"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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,"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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,"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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,"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2009,10,22]]},"reference":[{"key":"atypb1","volume-title":"Discrete-event System Simulation","author":"Banks, J.","year":"2005"},{"key":"atypb2","volume-title":"Proceedings of the 2006 Winter Simulation Conference","author":"Law, A.M."},{"key":"atypb3","volume-title":"Proceedings of the 2004 Winter Simulation Conference","author":"Balci, O."},{"key":"atypb4","volume-title":"Proceedings of the 2003 Winter Simulation Conference","author":"Balci, O."},{"key":"atypb5","volume-title":"Proceedings of the 2002 Winter Simulation Conference","author":"Balci, O."},{"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"},{"key":"atypb8","volume-title":"Proceedings of the 2005 Winter Simulation Conference","author":"Sargent, R.G."},{"key":"atypb9","unstructured":"J-Sim. http:\/\/www.j-sim.org\/ ."},{"key":"atypb10","volume-title":"Physical implementation of ad hoc network routing protocols using unmodified ns-2 models","author":"Saha, A.K.","year":"2004"},{"key":"atypb11","first-page":"99","author":"Perkins, C.E.","year":"1999","journal-title":"Proceedings of IEEE WMCSA\u2019"},{"key":"atypb12","author":"Perkins, C.","year":"2002","journal-title":"IETF Draft"},{"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"},{"key":"atypb16","volume-title":"Verification of Simulation Models of Network Protocols Using State Space Exploration. PhD thesis, Department of Computer Science","author":"Sobeih, A.","year":"2008"},{"key":"atypb17","volume-title":"Java PathFinder (JPF)"},{"key":"atypb18","first-page":"00","author":"Visser, W.","journal-title":"Proceedings of IEEE ASE\u2019"},{"key":"atypb19","volume-title":"Model Checking","author":"Clarke, E.M.","year":"1999"},{"key":"atypb20","volume-title":"Design, Realization and Evaluation of a Component-based Compositional Software Architecture for Network Simulation. PhD thesis","author":"Tyan, H.-Y.","year":"2002"},{"key":"atypb21","volume-title":"Communication and Concurrency","author":"Milner, R.","year":"1989"},{"key":"atypb22","first-page":"06","author":"Dwyer, M.B.","year":"2006","journal-title":"Proceedings of ACM FSE\u2019"},{"key":"atypb23","first-page":"07","author":"Dwyer, M.B.","journal-title":"Proceedings of ICSE\u2019"},{"key":"atypb24","volume-title":"The Art of Computer Programming, volume 2: Seminumerical Algorithms","author":"Knuth, D.E.","year":"1998"},{"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"},{"key":"atypb27","volume-title":"Proceedings of the IEEE International Conference on Automated Software Engineering","author":"Iosif, R."},{"key":"atypb28","volume-title":"Java Native Interface: Programmer\u2019s Guide and Specification"},{"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"},{"key":"atypb39","author":"Yang, C.H.","year":"1998","journal-title":"Proceedings of ACM\/IEE DAC\u2019 98"},{"key":"atypb40","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0130-9"},{"key":"atypb41","author":"Sobeih, A.","year":"2007","journal-title":"Proceedings of IEEE IPDPS 2007, NSF Next Generation Software Program Workshop"},{"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"},{"key":"atypb44","volume-title":"Symbolic Analysis Laboratory"},{"key":"atypb45","first-page":"92","author":"Dill, D.L.","journal-title":"Proceedings of IEEE ICCD\u2019"},{"key":"atypb46","volume-title":"Proceedings of the 2003 Winter Simulation Conference","author":"Rue\u00df, H."},{"key":"atypb47","first-page":"00","author":"Park, D.Y.W.","year":"2000","journal-title":"Proceedings of IEEE ASE\u2019"},{"key":"atypb48","first-page":"99","author":"Havelund, K.","journal-title":"Proceedings of SPIN\u2019"},{"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"},{"key":"atypb52","volume-title":"The Network Simulator-ns-2"},{"key":"atypb53","first-page":"99","author":"Kim, M.","journal-title":"Proceedings of ECRTS\u2019"},{"key":"atypb54","volume-title":"Theory of Modeling and Simulation","author":"Zeigler, B.P.","year":"2000","edition":"2"},{"key":"atypb55","author":"Spivey, M.","year":"1992","journal-title":"International Series in Computer Science"},{"key":"atypb56","volume-title":"Proceedings of the 2006 Winter Simulation Conference","author":"Traore, M.K."},{"key":"atypb57","volume-title":"ZUM \u201997: Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation","author":"Saaltink, M."},{"key":"atypb58","volume-title":"Proceedings of the 2006 Winter Simulation Conference","author":"Martens, J."},{"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"},{"key":"atypb61","volume-title":"Maude"},{"key":"atypb62","volume-title":"Maude 2.3 manual","author":"Clavel, M.","year":"2007"},{"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"},{"key":"atypb65","first-page":"96","author":"Cleaveland, R.","journal-title":"Proceedings of CAV\u2019"},{"key":"atypb66","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"Stewart, W.J.","year":"1994"},{"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":[[2026,5,1]],"date-time":"2026-05-01T11:22:05Z","timestamp":1777634525000},"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":[{"value":"0037-5497","type":"print"},{"value":"1741-3133","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,10,22]]}}}