{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:56:51Z","timestamp":1725742611153},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642402289"},{"type":"electronic","value":"9783642402296"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40229-6_9","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T21:47:40Z","timestamp":1374529660000},"page":"121-136","source":"Crossref","is-referenced-by-count":6,"title":["Quantitative Analysis of AODV and Its Variants on Dynamic Topologies Using Statistical Model Checking"],"prefix":"10.1007","author":[{"given":"Peter","family":"H\u00f6fner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maryam","family":"Kamali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"9_CR1","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.A.: Formal verification of standards for distance vector routing protocols. J. ACM\u00a049(4), 538\u2013576 (2002)","journal-title":"J. ACM"},{"key":"9_CR2","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., Guldstrand Larsen, K., 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":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bulychev, P., David, A., Larsen, K., Miku\u010dionis, M., B\u00f8gsted Poulson, 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. EPTCS, vol.\u00a085, pp. 1\u201316. Open Publishing Association (2012)","DOI":"10.4204\/EPTCS.85.1"},{"key":"9_CR4","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":"9_CR5","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-540-88562-7_18","volume-title":"Computational Methods in Systems Biology","author":"E.M. Clarke","year":"2008","unstructured":"Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical Model Checking in BioLab: Applications to the automated analysis of T-cell receptor signaling pathway. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol.\u00a05307, pp. 231\u2013250. Springer, Heidelberg (2008)"},{"key":"9_CR6","unstructured":"Clausen, T., Colin de Verdi\u00e9re, A., Yi, J., Niktash, A., Igarashi, Y., Satoh, H., Herberg, U., Lavenu, C., Lys, T., Perkins, C., Dean, J.: The lightweight on-demand ad hoc distance-vector routing protocol - next generation (LOADng). Internet Draft (Standards Track) (2013), \n                  \n                    http:\/\/tools.ietf.org\/html\/draft-clausen-lln-loadng-08"},{"key":"9_CR7","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":"9_CR8","unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Tech. Rep. 5513, NICTA (2013), \n                  \n                    http:\/\/www.nicta.com.au\/pub?id=5513"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-40196-1_32","volume-title":"QEST 2013","author":"A. Fehnker","year":"2013","unstructured":"Fehnker, A., H\u00f6fner, P., Kamali, M., Mehta, V.: Topology-based mobility models for wireless networks. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol.\u00a08054, pp. 389\u2013404. Springer, Heidelberg (2013)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"H\u00f6fner, P., van Glabbeek, R., Tan, W., Portmann, M., McIver, A., Fehnker, A.: A rigorous analysis of AODV and its variants. In: Modeling, Analysis and Simulation of Wireless and Mobile Systems, MSWIM 2012, pp. 203\u2013212. ACM (2012)","DOI":"10.1145\/2387238.2387274"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-642-38088-4_22","volume-title":"NASA Formal Methods","author":"P. H\u00f6fner","year":"2013","unstructured":"H\u00f6fner, P., McIver, A.: Statistical model checking of wireless mesh routing protocols. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol.\u00a07871, pp. 322\u2013336. Springer, Heidelberg (2013)"},{"key":"9_CR12","unstructured":"IEEE P802.11s: IEEE draft standard for information technology\u2014telecommunications and information exchange between systems\u2014local and metropolitan area networks\u2014specific requirements\u2014part 11: Wireless LAN Medium Access Control (MAC) and physical layer (PHY) specifications-amendment 10: Mesh networking (July 2010)"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-03845-7_15","volume-title":"Computational Methods in Systems Biology","author":"S.K. Jha","year":"2009","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol.\u00a05688, pp. 218\u2013234. Springer, Heidelberg (2009)"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: a pragmatic approach to model checking real code. In: Operating Systems Design and Implementation, OSDI 2002 (2002)","DOI":"10.1145\/1060289.1060297"},{"key":"9_CR15","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":"9_CR16","unstructured":"Perkins, C., Chakeres, I.: Dynamic MANET on-demand (AODVv2) routing. Internet Draft (Standards Track) (2013), \n                  \n                    http:\/\/tools.ietf.org\/html\/draft-ietf-manet-dymo-25"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Perkins, C., Royer, E.: Ad-hoc On-Demand Distance Vector Routing. In: 2nd IEEE Workshop on Mobile Computing Systems and Applications, pp. 90\u2013100 (1999)","DOI":"10.1109\/MCSA.1999.749281"},{"key":"9_CR18","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 (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"9_CR19","unstructured":"Younes, H.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon University (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40229-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T22:51:49Z","timestamp":1557960709000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40229-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642402289","9783642402296"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40229-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}