{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:15:11Z","timestamp":1772835311250,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642380877","type":"print"},{"value":"9783642380884","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38088-4_22","type":"book-chapter","created":{"date-parts":[[2013,5,9]],"date-time":"2013-05-09T00:38:27Z","timestamp":1368059907000},"page":"322-336","source":"Crossref","is-referenced-by-count":19,"title":["Statistical Model Checking of Wireless Mesh Routing Protocols"],"prefix":"10.1007","author":[{"given":"Peter","family":"H\u00f6fner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Annabelle","family":"McIver","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Amin, M., Abrar, M., Khan, Z.U., Andusalam, Rizwan, S.: Comparison of OLSR & DYMO routing protocols on the basis of different performance metrics in mobile ad-hoc networks. American Journal of Scientific Research (2011)"},{"issue":"4","key":"22_CR2","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1145\/581771.581775","volume":"49","author":"K. Bhargavan","year":"2002","unstructured":"Bhargavan, K., Obradovic, D., Gunter, C.: Formal verification of standards for distance vector routing protocols. J. ACM\u00a049(4), 538\u2013576 (2002)","journal-title":"J. ACM"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-642-28891-3_39","volume-title":"NASA Formal Methods","author":"P. Bulychev","year":"2012","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., B\u00f8gsted Poulsen, D.: Checking and distributing statistical model checking. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 449\u2013463. Springer, Heidelberg (2012)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Bulychev, P., David, A., Larsen, K., Miku\u010dionis, M., B\u00f8gsted Poulsen, D., Legay, A., Wang, Z.: UPPAAL-SMC: Statistical model checking for priced timed automata. In: Wiklicky, H., Massink, M. (eds.) Quantitative Aspects of Programming Languages and Systems. EPTCS, vol.\u00a085, pp. 1\u201316. Open Publishing Association (2012)","DOI":"10.4204\/EPTCS.85.1"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/11494881_20","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"S. Chiyangwa","year":"2005","unstructured":"Chiyangwa, S., Kwiatkowska, M.: A timing analysis of AODV. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol.\u00a03535, pp. 306\u2013321. Springer, Heidelberg (2005)"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Edenhofer, S., H\u00f6fner, P.: Towards a rigorous analysis of AODVv2 (DYMO). In: Rigorous Protocol Engineering (W-RiPE 2012). IEEE Press (2012)","DOI":"10.1109\/ICNP.2012.6459942"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-68746-7_13","volume-title":"Applications and Theory of Petri Nets","author":"K.L. Espensen","year":"2008","unstructured":"Espensen, K.L., Kjeldsen, M.K., Kristensen, L.M.: Modelling and initial validation of the DYMO routing protocol for mobile ad-hoc networks. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol.\u00a05062, pp. 152\u2013170. Springer, Heidelberg (2008)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-28756-5_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Fehnker","year":"2012","unstructured":"Fehnker, A., van Glabbeek, R., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 173\u2013187. Springer, Heidelberg (2012)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J., H\u00f6fner, P., Tan, W.L., Portmann, M.: Sequence numbers do not guarantee loop freedom\u2014AODV can yield routing loops (2012), \n                    \n                      http:\/\/rvg.web.cse.unsw.edu.au\/pub\/AODVloop.pdf","DOI":"10.1145\/2507924.2507943"},{"issue":"1-2","key":"22_CR10","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/s11036-008-0048-2","volume":"13","author":"D. Johnson","year":"2008","unstructured":"Johnson, D., Lysko, A.: Comparison of MANET routing protocols using a scaled indoor wireless grid. Mob. Netw. Appl.\u00a013(1-2), 82\u201396 (2008)","journal-title":"Mob. Netw. Appl."},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Kum, D.W., Park, J.S., Cho, Y.Z., Cheon, B.Y.: Performance evaluation of AODV and DYMO routing protocols in MANET. In: Consumer Communications and Networking Conference (CCNC 2010), pp. 1046\u20131047. IEEE Press (2010)","DOI":"10.1109\/CCNC.2010.5421657"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Milic, B., Malek, M.: NPART\u2014node placement algorithm for realistic topologies in wireless multihop network simulation. In: Simulation Tools and Techniques (Simutools 2009), pp. 9:1\u20139:10. ICST (2009)","DOI":"10.4108\/ICST.SIMUTOOLS2009.5669"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Miskovic, S., Knightly, E.: Routing primitives for wireless mesh networks: Design, analysis and experiments. In: Conference on Information communications (INFOCOM 2010), pp. 2793\u20132801. IEEE Press (2010)","DOI":"10.1109\/INFCOM.2010.5462111"},{"key":"22_CR14","unstructured":"Perkins, C., Belding-Royer, E., Das, S.: Ad hoc on-demand distance vector (AODV) routing. RFC 3561 (Experimental) (2003), \n                    \n                      http:\/\/www.ietf.org\/rfc\/rfc3561"},{"key":"22_CR15","unstructured":"Perkins, C., Chakeres, I.: Dynamic MANET on-demand (AODVv2) routing. IETF Internet Draft (Work in Progress) (March 2012), \n                    \n                      http:\/\/tools.ietf.org\/html\/draft-ietf-manet-dymo-22"},{"key":"22_CR16","unstructured":"R Core Team: R: A Language and Environment for Statistical Computing (2012), \n                    \n                      http:\/\/www.R-project.org"},{"key":"22_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1155\/2010\/373759","volume":"31","author":"M. Saleem","year":"2010","unstructured":"Saleem, M., Khayam, S.A., Farooq, M.: On performance modeling of ad hoc routing protocols. EURASIP J. Wirel. Commun. Netw. 2010, 31:1\u201331:13 (2010)","journal-title":"EURASIP J. Wirel. Commun. Netw."},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Schuts, M., Zhu, F., Heidarian, F., Vaandrager, F.: Modelling clock synchronization in the Chess gMAC WSN protocol. In: Andova, S., McIver, A., D\u2019Argenio, P., Cuijpers, P., Markovski, J., Morgan, C., N\u00fa\u00f1ez, M. (eds.) Quantitative Formal Methods: Theory and Applications (QFM 2009). EPTCS, vol.\u00a013, pp. 41\u201354 (2009)","DOI":"10.4204\/EPTCS.13.4"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: Vesta: A statistical model-checker and analyzer for probabilistic systems. In: Quantitative Evaluaiton of Systems (QEST 2005), pp. 251\u2013252. IEEE Press (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"22_CR20","unstructured":"Younes, H.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon University (2004)"},{"issue":"2","key":"22_CR21","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/2185376.2185383","volume":"42","author":"P. Zave","year":"2012","unstructured":"Zave, P.: Using lightweight modeling to understand CHORD. SIGCOMM Comput. Commun. Rev.\u00a042(2), 49\u201357 (2012)","journal-title":"SIGCOMM Comput. Commun. Rev."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38088-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T23:48:13Z","timestamp":1557704893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38088-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642380877","9783642380884"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38088-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}