{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:23:09Z","timestamp":1772835789911,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642287558","type":"print"},{"value":"9783642287565","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_13","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T16:57:15Z","timestamp":1332435435000},"page":"173-187","source":"Crossref","is-referenced-by-count":50,"title":["Automated Analysis of AODV Using UPPAAL"],"prefix":"10.1007","author":[{"given":"Ansgar","family":"Fehnker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rob","family":"van Glabbeek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Annabelle","family":"McIver","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Portmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wee Lum","family":"Tan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","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.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"issue":"4","key":"13_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.A.: Formal verification of standards for distance vector routing protocols. J. ACM\u00a049(4), 538\u2013576 (2002)","journal-title":"J. ACM"},{"key":"13_CR3","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":"13_CR4","unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) European Symposium on Programming (ESOP 2012). Springer, Heidelberg (in press, 2012)"},{"key":"13_CR5","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 (2012), \n                    \n                      http:\/\/www.nicta.com.au\/pub?id=5513"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A.K., Portmann, M., Tan, W.L.: Modelling and analysis of AODV in UPPAAL. In: 1st International Workshop on Rigorous Protocol Engineering (2011)","DOI":"10.1007\/978-3-642-28756-5_13"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-73210-5_14","volume-title":"Integrated Formal Methods","author":"A. Fehnker","year":"2007","unstructured":"Fehnker, A., van Hoesel, L., Mader, A.: Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 253\u2013272. Springer, Heidelberg (2007)"},{"issue":"1","key":"13_CR8","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1109\/MWC.2010.5416357","volume":"17","author":"G.R. Hiertz","year":"2010","unstructured":"Hiertz, G.R., Denteneer, D., Max, S., Taori, R., Cardona, J., Berlemann, L., Walke, B.: IEEE 802.11s: the WLAN mesh standard. IEEE Wireless Communications\u00a017(1), 104\u2013111 (2010)","journal-title":"IEEE Wireless Communications"},{"issue":"1-2","key":"13_CR9","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal of Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal of Software Tools for Technology Transfer"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Miskovic, S., Knightly, E.W.: Routing primitives for wireless mesh networks: Design, analysis and experiments. In: IEEE INFOCOM, pp. 2793\u20132801 (2010), \n                    \n                      http:\/\/dx.doi.org\/10.1109\/INFCOM.2010.5462111","DOI":"10.1109\/INFCOM.2010.5462111"},{"key":"13_CR11","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":"13_CR12","doi-asserted-by":"crossref","unstructured":"Perkins, C., Belding-Royer, E., Das, S.: Ad hoc on-demand distance vector (AODV) routing. RFC 3561 (2003), \n                    \n                      http:\/\/www.ietf.org\/rfc\/rfc3561.txt","DOI":"10.17487\/rfc3561"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"de Renesse, R., Aghvami, A.H.: Formal verification of ad hoc routing protocols using SPIN model checker. In: Proceedings of IEEE MELECON 2004, pp. 1177\u20131182. IEEE (2004)","DOI":"10.1109\/MELCON.2004.1348275"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-540-30232-2_22","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"O. Wibling","year":"2004","unstructured":"Wibling, O., Parrow, J., Pears, A.N.: Automatized Verification of Ad Hoc Routing Protocols. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol.\u00a03235, pp. 343\u2013358. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T20:19:09Z","timestamp":1556482749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}