{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:14:32Z","timestamp":1772835272450,"version":"3.50.1"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319175232","type":"print"},{"value":"9783319175249","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17524-9_9","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"112-126","source":"Crossref","is-referenced-by-count":7,"title":["Statistical Model Checking of Ad Hoc Routing Protocols in Lossy Grid Networks"],"prefix":"10.1007","author":[{"given":"Alice","family":"Dal Corso","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damiano","family":"Macedonio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Merro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: International Conference on the Quantitative Evaluation of Systems (QEST), pp. 125\u2013126. IEEE Computer Society (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Benetti, D., Merro, M., Vigano, L.: Model checking ad hoc network routing protocols: Aran vs. endairA. In: 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM), pp. 191\u2013202. IEEE Computer Society (2010)","DOI":"10.1109\/SEFM.2010.24"},{"key":"9_CR3","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. Journal of the ACM 49, 538\u2013576 (2002)","journal-title":"Journal of the ACM"},{"key":"9_CR4","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. 7226, pp. 449\u2013463. Springer, Heidelberg (2012)"},{"key":"9_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. 3535, pp. 306\u2013321. Springer, Heidelberg (2005)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Clausen, T., Jacquet, P.: Optimized Link State Routing Protocol (OLSR), rFC 3626 (2003)","DOI":"10.17487\/rfc3626"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-24310-3_7","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80\u201396. Springer, Heidelberg (2011)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","volume-title":"Computer Aided Verification","author":"A David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349\u2013355. Springer, Heidelberg (2011)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Edenhofer, S., H\u00f6fner, P.: Towards a rigorous analysis of AODVv2 (DYMO). In: IEEE International Conference on Network Protocols (ICNP), pp. 1\u20136. IEEE Computer Society (2012)","DOI":"10.1109\/ICNP.2012.6459942"},{"key":"9_CR10","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)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-642-40229-6_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P H\u00f6fner","year":"2013","unstructured":"H\u00f6fner, P., Kamali, M.: Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 121\u2013136. Springer, Heidelberg (2013)"},{"key":"9_CR12","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)"},{"key":"9_CR13","unstructured":"Johnson, D.B., Maltz, D.A.: Dynamic Source Routing in Ad Hoc Wireless Networks. Kluwer Acad. Pub. (1996)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-319-12904-4_9","volume-title":"Rewriting Logic and Its Applications","author":"S Liu","year":"2014","unstructured":"Liu, S., \u00d6lveczky, P.C., Meseguer, J.: A framework for mobile Ad hoc networks in real-time maude. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 162\u2013177. Springer, Heidelberg (2014)"},{"issue":"5","key":"9_CR15","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1007\/s00165-011-0210-7","volume":"25","author":"M Merro","year":"2013","unstructured":"Merro, M., Sibilio, E.: A calculus of trustworthy ad hoc networks. Formal Aspects of Computing 25(5), 801\u2013832 (2013)","journal-title":"Formal Aspects of Computing"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Miskovic, S., Knightly, E.: Routing primitives for wireless mesh networks: design, analysis and experiments. In: IEEE International Conference on Computer Communications (INFOCOM), pp. 2793\u20132801. IEEE Computer Society (2010)","DOI":"10.1109\/INFCOM.2010.5462111"},{"key":"9_CR17","unstructured":"Perkins, C., Belding-Royer, E., Das, S.: Ad-hoc on-demand distance vector (AODV). RFC 3561 (Experimental) (2003). http:\/\/www.ietf.org\/rfc\/rfc3561"},{"key":"9_CR18","unstructured":"Perkins, C., Chakeres, I.: Dynamic MANET on-demand (AODVv2) routing. IETF Internet Draft (2012, Work in Progress)"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Perkins, C.E., Bhagwat, P.: Highly dynamic destination-sequenced distance-vector routing (DSDV) for mobile computers. In: Conference on Communications Architectures, Protocols and Applications (SIGCOMM), pp. 234\u2013244 (1994)","DOI":"10.1145\/190809.190336"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: VESTA: A statistical model-checker and analyzer for probabilistic systems. In: International Conference on the Quantitative Evaluation of Systems (QEST), pp. 251\u2013252. IEEE Computer Society (2005)","DOI":"10.1109\/QEST.2005.42"},{"key":"9_CR21","unstructured":"Younes, H., S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon University (2004)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T23:26:22Z","timestamp":1747869982000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}