{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:19:10Z","timestamp":1772835550895,"version":"3.50.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319731162","type":"print"},{"value":"9783319731179","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,12,22]],"date-time":"2017-12-22T00:00:00Z","timestamp":1513900800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-73117-9_24","type":"book-chapter","created":{"date-parts":[[2017,12,21]],"date-time":"2017-12-21T16:45:34Z","timestamp":1513874734000},"page":"337-350","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["AODVv2: Performance vs. Loop Freedom"],"prefix":"10.1007","author":[{"given":"Mojgan","family":"Kamali","sequence":"first","affiliation":[]},{"given":"Massimo","family":"Merro","sequence":"additional","affiliation":[]},{"given":"Alice","family":"Dal Corso","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,22]]},"reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-40213-5_11","volume-title":"Fundamentals of Software Engineering","author":"L Battisti","year":"2013","unstructured":"Battisti, L., Macedonio, D., Merro, M.: Statistical model checking of a clock synchronization protocol for sensor networks. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 168\u2013182. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40213-5_11"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Benetti, D., Merro, M., Vigan\u00f2, L.: Model checking ad hoc network routing protocols: ARAN vs. endairA. In: SEFM 2010, pp. 191\u2013202. IEEE (2010)","DOI":"10.1109\/SEFM.2010.24"},{"issue":"4","key":"24_CR4","doi-asserted-by":"crossref","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 49(4), 538\u2013576 (2002)","journal-title":"J. ACM"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-662-49498-1_5","volume-title":"Programming Languages and Systems","author":"E Bres","year":"2016","unstructured":"Bres, E., van Glabbeek, R., H\u00f6fner, P.: A timed process algebra for wireless networks with an application in routing. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 95\u2013122. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_5"},{"key":"24_CR6","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-17524-9_9","volume-title":"NASA Formal Methods","author":"A Dal Corso","year":"2015","unstructured":"Dal Corso, A., Macedonio, D., Merro, M.: Statistical model checking of Ad Hoc routing protocols in lossy grid networks. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 112\u2013126. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_9"},{"issue":"4","key":"24_CR8","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u0103ionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397\u2013415 (2015)","journal-title":"STTT"},{"key":"24_CR9","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. 7214, pp. 173\u2013187. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_13"},{"key":"24_CR10","doi-asserted-by":"crossref","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. CoRR abs\/1312.7645 (2013)","DOI":"10.1007\/978-3-642-28869-2_15"},{"issue":"4","key":"24_CR11","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1145\/75247.75268","volume":"19","author":"JJ Garcia-Luna-Aceves","year":"1989","unstructured":"Garcia-Luna-Aceves, J.J.: A unified approach to loop-free routing using distance vectors or link states. SIGCOMM Comput. Commun. Rev. 19(4), 212\u2013223 (1989)","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Garcia-Luna-Aceves, J.J., Rangarajan, H.: A new framework for loop-free on-demand routing using destination sequence numbers. In: MASS 2004, pp. 426\u2013435. IEEE (2004)","DOI":"10.1109\/MAHSS.2004.1392182"},{"issue":"4","key":"24_CR13","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s00446-015-0262-7","volume":"29","author":"R Glabbeek van","year":"2016","unstructured":"van Glabbeek, R., H\u00f6fner, P., Portmann, M., Tan, W.L.: Modelling and verifying the AODV routing protocol. Distrib. Comput. 29(4), 279\u2013315 (2016)","journal-title":"Distrib. Comput."},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R., H\u00f6fner, P., Tan, W.L., Portmann, M.: Sequence numbers do not guarantee loop freedom: AODV can yield routing loops. In: MSWiM 2013, pp. 91\u2013100. ACM (2013)","DOI":"10.1145\/2507924.2507943"},{"key":"24_CR15","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. 7871, pp. 322\u2013336. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_22"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Kamali, M., Merro, M., Dal Corso, A.: AODVv2: performance vs. loop freedom. Technical report. pp. 1177. TUCS - Turku Centre for Computer Science (2016)","DOI":"10.1007\/978-3-319-73117-9_24"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-319-22969-0_13","volume-title":"Software Engineering and Formal Methods","author":"M Kamali","year":"2015","unstructured":"Kamali, M., H\u00f6fner, P., Kamali, M., Petre, L.: Formal analysis of proactive, distributed routing. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 175\u2013189. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_13"},{"issue":"47","key":"24_CR18","doi-asserted-by":"crossref","first-page":"6585","DOI":"10.1016\/j.tcs.2011.07.016","volume":"412","author":"M Merro","year":"2011","unstructured":"Merro, M., Ballardin, F., Sibilio, E.: A timed calculus for wireless systems. TCS 412(47), 6585\u20136611 (2011)","journal-title":"TCS"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Miskovic, S., Knightly, E.W.: Routing primitives for wireless mesh networks: design, analysis and experiments. In: INFOCOM 2010, pp. 1\u20139. IEEE Press (2010)","DOI":"10.1109\/INFCOM.2010.5462111"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-19195-9_7","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"KS Namjoshi","year":"2015","unstructured":"Namjoshi, K.S., Trefler, R.J.: Loop freedom in AODVv2. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 98\u2013112. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19195-9_7"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Perkins, C., Belding-Royer, E., Das, S.: Ad hoc on-demand distance vector (AODV) Routing. RFC 3561 (Experimental) (2003)","DOI":"10.17487\/rfc3561"},{"key":"24_CR22","unstructured":"Perkins, C., Stan, R., Dowdell, J.: Dynamic MANET on-demand (AODVv2) Routing draft-ietf-manet-dymo. Internet Draft 26 (2013)"},{"key":"24_CR23","unstructured":"Perkins, C., Stan, R., Dowdell, J., Steenbrink, L., Mercieca, V.: Ad Hoc On-demand Distance Vector (AODVv2) Routing draft-ietf-manet-aodvv2. Internet Draft 11 (2015)"},{"key":"24_CR24","unstructured":"Perkins, C., Stan, R., Dowdell, J., Steenbrink, L., Mercieca, V.: Dynamic MANET On-demand (AODVv2) Routing draft-ietf-manet-aodvv2. Internet Draft 16 (2016)"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.A.: Vesta: a statistical model-checker and analyzer for probabilistic systems. In: QEST 2005, pp. 251\u2013252. IEEE (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"24_CR26","unstructured":"Yousefi, B., Ghassemi, F., Khosravi, R.: Modeling and efficient verification of wireless ad hoc networks. CoRR abs\/1604.07179 (2016)"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2018: Theory and Practice of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73117-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T11:46:04Z","timestamp":1570535164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73117-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,22]]},"ISBN":["9783319731162","9783319731179"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73117-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,22]]}}}