{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T11:07:20Z","timestamp":1772795240998,"version":"3.50.1"},"reference-count":197,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,12,15]],"date-time":"2025-12-15T00:00:00Z","timestamp":1765756800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,12,15]],"date-time":"2025-12-15T00:00:00Z","timestamp":1765756800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2026,2]]},"DOI":"10.1007\/s10703-025-00490-5","type":"journal-article","created":{"date-parts":[[2025,12,15]],"date-time":"2025-12-15T14:36:50Z","timestamp":1765809410000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal methods for mobile ad hoc networks: a survey"],"prefix":"10.1007","volume":"68","author":[{"given":"Wan","family":"Fokkink","sequence":"first","affiliation":[]},{"given":"Rob","family":"van Glabbeek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,12,15]]},"reference":[{"issue":"1","key":"490_CR1","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1109\/PROC.1987.13702","volume":"75","author":"J Jubin","year":"1987","unstructured":"Jubin J, Tornow JD (1987) The DARPA packet radio network protocols. Proc IEEE 75(1):21\u201332. https:\/\/doi.org\/10.1109\/PROC.1987.13702","journal-title":"Proc IEEE"},{"issue":"1","key":"490_CR2","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1109\/PROC.1987.13707","volume":"75","author":"N Shacham","year":"1987","unstructured":"Shacham N, Westcott J (1987) Future directions in packet radio architectures and protocols. Proc IEEE 75(1):83\u201399. https:\/\/doi.org\/10.1109\/PROC.1987.13707","journal-title":"Proc IEEE"},{"issue":"3","key":"490_CR3","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1023\/A:1019108612308","volume":"5","author":"SR Das","year":"2000","unstructured":"Das SR, Casta\u00f1eda R, Yan J (2000) Simulation-based performance evaluation of routing protocols for mobile ad hoc networks. Mob Networks Appl 5(3):179\u2013189. https:\/\/doi.org\/10.1023\/A:1019108612308","journal-title":"Mob Networks Appl"},{"key":"490_CR4","doi-asserted-by":"publisher","unstructured":"Cavin D, Sasson Y, Schiper A (2002) On the accuracy of MANET simulators. In: Proceedings 1st Workshop on Principles of Mobile Computing (POMC), ACM, New York, pp 38\u201343. https:\/\/doi.org\/10.1145\/584490.584499","DOI":"10.1145\/584490.584499"},{"key":"490_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-38800-3","volume-title":"Formal methods for software engineering: languages, methods, application domains","author":"M Roggenbach","year":"2022","unstructured":"Roggenbach M, Schlingloff B-H, Schneider G (2022) Formal methods. In: Roggenbach M, Cerone A, Schlingloff B-H, Schneider G, Shaikh SA (eds) Formal methods for software engineering: languages, methods, application domains. Springer, Heidelberg, pp 1\u201346. https:\/\/doi.org\/10.1007\/978-3-030-38800-3"},{"issue":"1","key":"490_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3522582","volume":"34","author":"T Kulik","year":"2022","unstructured":"Kulik T, Dongol B, Larsen PG, Macedo HD, Schneider S, Tran-J\u00f8rgensen PWV, Woodcock J (2022) A survey of practical formal methods for security. Formal Aspects Comput 34(1):1\u201339. https:\/\/doi.org\/10.1145\/3522582","journal-title":"Formal Aspects Comput"},{"key":"490_CR7","volume-title":"Optimized link state routing protocol (OLSR). RFC 3626. IETF","author":"TH Clausen","year":"2003","unstructured":"Clausen TH, Jacquet P (2003) Optimized link state routing protocol (OLSR). RFC 3626. IETF. http:\/\/www.ietf.org\/rfc\/rfc3626"},{"key":"490_CR8","doi-asserted-by":"publisher","unstructured":"Perkins CE, Royer EM (1999) Ad-hoc on-demand distance vector routing. In: Proceedings 2nd Workshop on Mobile Computer Systems and Applications (WMCSA), IEEE, New York, pp 90\u2013100. https:\/\/doi.org\/10.1109\/MCSA.1999.749281","DOI":"10.1109\/MCSA.1999.749281"},{"key":"490_CR9","volume-title":"Ad hoc on-demand distance vector (AODV) routing. RFC 3561. IETF","author":"CE Perkins","year":"2003","unstructured":"Perkins CE, Royer EM, Das SR (2003) Ad hoc on-demand distance vector (AODV) routing. RFC 3561. IETF. https:\/\/datatracker.ietf.org\/doc\/html\/rfc3561"},{"key":"490_CR10","doi-asserted-by":"publisher","unstructured":"Das S, Dill DL (2002) Counter-example based predicate discovery in predicate abstraction. In: Proceedings 4th Conference on Formal Methods in Computer-Aided Design (FMCAD). LNCS, vol 2517. Springer, Heidelberg, pp 19\u201332. https:\/\/doi.org\/10.1007\/3-540-36126-X_2","DOI":"10.1007\/3-540-36126-X_2"},{"key":"490_CR11","doi-asserted-by":"publisher","unstructured":"Engler DR, Musuvathi M (2004) Static analysis versus software model checking for bug finding. In: Proceedings 5th Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol 2937. Springer, Heidelberg, pp 191\u2013210. https:\/\/doi.org\/10.1007\/978-3-540-24622-0_17","DOI":"10.1007\/978-3-540-24622-0_17"},{"issue":"4","key":"490_CR12","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 CA (2002) Formal verification of standards for distance vector routing protocols. JACM 49(4):538\u2013576. https:\/\/doi.org\/10.1145\/581771.581775","journal-title":"JACM"},{"issue":"5","key":"490_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The model checker spin. IEEE Trans Softw Eng 23(5):279\u2013295. https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans Softw Eng"},{"key":"490_CR14","volume-title":"Introduction to hol: a theorem proving environment for higher order logic","year":"1993","unstructured":"Gordon MJC, Melham TF (eds. (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge"},{"key":"490_CR15","doi-asserted-by":"publisher","unstructured":"Fehnker A, van Glabbeek RJ, H\u00f6fner P, McIver A, Portmann M, Tan WL (2013) A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical Report 5513, NICTA. https:\/\/doi.org\/10.48550\/arXiv.1312.7645","DOI":"10.48550\/arXiv.1312.7645"},{"key":"490_CR16","doi-asserted-by":"publisher","unstructured":"Wu X, Xu Q, Zhu H (2013) Formal analysis of AODV using rely-guarantee. In: Proceedings 7th Symposium on Theoretical Aspects of Software Engineering (TASE), IEEE, New York, pp 45\u201348. https:\/\/doi.org\/10.1109\/TASE.2013.14","DOI":"10.1109\/TASE.2013.14"},{"key":"490_CR17","doi-asserted-by":"publisher","unstructured":"Zhou M, Yang H, Zhang X, Wang J (2009) The proof of AODV loop freedom. In: Proceedings 1st Conference on Wireless Communications and Signal Processing (WCSP), ACM, New York, pp 1\u20135. https:\/\/doi.org\/10.1109\/WCSP.2009.5371479","DOI":"10.1109\/WCSP.2009.5371479"},{"key":"490_CR18","doi-asserted-by":"publisher","unstructured":"van Glabbeek RJ, H\u00f6fner P, Tan WL, Portmann M (2013) Sequence numbers do not guarantee loop freedom: AODV can yield routing loops. In: Proceedings 16th Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM), ACM, New York, pp 91\u2013100. https:\/\/doi.org\/10.1145\/2507924.2507943","DOI":"10.1145\/2507924.2507943"},{"key":"490_CR19","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(81)90049-9","volume":"14","author":"K Jensen","year":"1981","unstructured":"Jensen K (1981) Coloured petri nets and the invariant-method. Theor Comput Sci 14:317\u2013336. https:\/\/doi.org\/10.1016\/0304-3975(81)90049-9","journal-title":"Theor Comput Sci"},{"key":"490_CR20","volume-title":"Dynamic MANET on-demand (AODVv2) routing. Draft. IETF","author":"CE Perkins","year":"2013","unstructured":"Perkins CE, Ratliff S, Dowdell J (2013) Dynamic MANET on-demand (AODVv2) routing. Draft. IETF. https:\/\/datatracker.ietf.org\/doc\/html\/draft-ietf-manet-aodvv2-02"},{"key":"490_CR21","unstructured":"Xiong C, Murata T, Tsai J (2002) Modeling and simulation of routing protocol for mobile ad hoc networks using colored petri nets. In: Proceedings Workshop on Formal Methods Applied to Defense Systems. Conferences in Research and Practice in Information Technology, vol 12. Australian Computer Society, Sydney, pp 145\u2013153. https:\/\/dl.acm.org\/doi\/abs\/10.5555\/846335.846350"},{"key":"490_CR22","doi-asserted-by":"publisher","unstructured":"Espensen KL, Kjeldsen MK, Kristensen LM (2008) Modelling and initial validation of the DYMO routing protocol for mobile ad-hoc networks. In: Proceedings 29th Conference on Applications and Theory of Petri Nets (PETRI NETS). LNCS, vol 5062. Springer, Heidelberg, pp 152\u2013170. https:\/\/doi.org\/10.1007\/978-3-540-68746-7_13","DOI":"10.1007\/978-3-540-68746-7_13"},{"key":"490_CR23","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-642-04856-2_5","volume":"3","author":"J Billington","year":"2009","unstructured":"Billington J, Yuan C (2009) On modelling and analysing the dynamic MANET on-demand (DYMO) routing protocol. Trans Petri Nets Other Model Concurr 3:98\u2013126. https:\/\/doi.org\/10.1007\/978-3-642-04856-2_5","journal-title":"Trans Petri Nets Other Model. Concurr."},{"key":"490_CR24","doi-asserted-by":"publisher","unstructured":"Edenhofer S, H\u00f6fner P (2012) Towards a rigorous analysis of AODVv2 (DYMO). In: Proceedings 20th Conference on Network Protocols (ICNP), IEEE, New York, pp 1\u20136. https:\/\/doi.org\/10.1109\/ICNP.2012.6459942","DOI":"10.1109\/ICNP.2012.6459942"},{"key":"490_CR25","doi-asserted-by":"publisher","unstructured":"Saksena M, Wibling O, Jonsson B (2008) Graph grammar modeling and verification of ad hoc routing protocols. In: Proceedings 14th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol 4963. Springer, Heidelberg, pp 18\u201332. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_3","DOI":"10.1007\/978-3-540-78800-3_3"},{"key":"490_CR26","doi-asserted-by":"publisher","unstructured":"Namjoshi KS, Trefler RJ (2015) Loop freedom in AODVv2. In: Proceedings 35th IFIP WG 6.1 Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE). LNCS, vol 9039. Springer, Heidelberg, pp 98\u2013112. https:\/\/doi.org\/10.1007\/978-3-319-19195-9_7","DOI":"10.1007\/978-3-319-19195-9_7"},{"issue":"6","key":"490_CR27","doi-asserted-by":"publisher","first-page":"1051","DOI":"10.1007\/s00165-017-0429-z","volume":"29","author":"B Yousefi","year":"2017","unstructured":"Yousefi B, Ghassemi F, Khosravi R (2017) Modeling and efficient verification of wireless ad hoc networks. Formal Aspects Comput 29(6):1051\u20131086. https:\/\/doi.org\/10.1007\/s00165-017-0429-z","journal-title":"Formal Aspects Comput"},{"key":"490_CR28","doi-asserted-by":"publisher","unstructured":"Zakiuddin I, Goldsmith M, Whittaker P, Gardiner PHB (2003) A methodology for model-checking ad-hoc networks. In: Proceedings 10th Workshop on Model Checking Software (SPIN). LNCS, vol 2648. Springer, Heidelberg, pp 181\u2013196. https:\/\/doi.org\/10.1007\/3-540-44829-2_12","DOI":"10.1007\/3-540-44829-2_12"},{"key":"490_CR29","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11423348_9","volume-title":"Communicating sequential processes: the first 25 years. LNCS","author":"J Lawrence","year":"2004","unstructured":"Lawrence J (2004) Practical application of CSP and FDR to software design. In: Communicating sequential processes: the first 25 years. LNCS, vol 3525. Springer, Heidelberg, pp 151\u2013174. https:\/\/doi.org\/10.1007\/11423348_9"},{"key":"490_CR30","volume-title":"Cluster based routing protocol (CBRP) functional specification. Draft. IETF","author":"M Jiang","year":"1998","unstructured":"Jiang M, Li J, Tay YC (1998) Cluster based routing protocol (CBRP) functional specification. Draft. IETF. https:\/\/tools.ietf.org\/id\/draft-ietf-manet-cbrp-spec-00.txt"},{"key":"490_CR31","doi-asserted-by":"publisher","unstructured":"Wibling O, Parrow J, Pears AN (2004) Automatized verification of ad hoc routing protocols. In: Proceedings 24th IFIP WG 6.1 Conference on Formal Techniques for Networked and Distributed Systems (FORTE). LNCS, vol 3235. Springer, Heidelberg, pp 343\u2013358. https:\/\/doi.org\/10.1007\/978-3-540-30232-2_22","DOI":"10.1007\/978-3-540-30232-2_22"},{"key":"490_CR32","unstructured":"Tschudin C, Gold R, Rensfelt O, Wibling O (2004) Lunar: a lightweight underlay network ad-hoc routing protocol and implementation. In: Proceedings 5th Conference on Next Generation Teletraffic and Wired\/Wireless Advanced Networking (NEW2AN), pp 38\u201343. https:\/\/www.researchgate.net\/publication\/228870993_LUNAR_a_lightweight_underlay_network_ad-hoc_routing_protocol_and_implementation"},{"key":"490_CR33","doi-asserted-by":"publisher","unstructured":"de Renesse R, Aghvami AH (2004) Formal verification of ad-hoc routing protocols using spin model checker. In: Proceedings 12th Mediterranean Electrotechnical Conference (IEEE MELECON), IEEE, New York, pp 1177\u20131182. https:\/\/doi.org\/10.1109\/MELCON.2004.1348275","DOI":"10.1109\/MELCON.2004.1348275"},{"key":"490_CR34","unstructured":"Khengar P, Aghvami AH (2001) WARP - The wireless adaptive routing protocol. In: Proceedings 10th IST Mobile Summit, pp 480\u2013485"},{"issue":"2","key":"490_CR35","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/j.csi.2005.01.017","volume":"28","author":"VA Oleshchuk","year":"2005","unstructured":"Oleshchuk VA (2005) Modeling, specification and verification of ad-hoc sensor networks using spin. Comput Stand Interface 28(2):159\u2013165. https:\/\/doi.org\/10.1016\/j.csi.2005.01.017","journal-title":"Comput Stand Interface"},{"key":"490_CR36","doi-asserted-by":"publisher","unstructured":"Steele MF, Andel TR (2012) Modeling the optimized link-state routing protocol for verification. In: Proceedings Spring Simulation Multiconference (SpringSim), SCS\/ACM, New York, pp 1\u20138. https:\/\/doi.org\/10.5555\/2346616.2346651","DOI":"10.5555\/2346616.2346651"},{"key":"490_CR37","doi-asserted-by":"publisher","unstructured":"C\u00e2mara D, Ferreira Loureiro AA, Filali F (2007) Methodology for formal verification of routing protocols for ad hoc wireless networks. In: Proceedings 8th Global Communications Conference (GLOBECOM), IEEE, New York, pp 705\u2013709. https:\/\/doi.org\/10.1109\/GLOCOM.2007.137","DOI":"10.1109\/GLOCOM.2007.137"},{"issue":"4","key":"490_CR38","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1023\/A:1019106118419","volume":"6","author":"Y Ko","year":"2000","unstructured":"Ko Y, Vaidya NH (2000) Location-aided routing (LAR) in mobile ad hoc networks. Wirel Networks 6(4):307\u2013321. https:\/\/doi.org\/10.1023\/A:1019106118419","journal-title":"Wirel Networks"},{"key":"490_CR39","doi-asserted-by":"publisher","unstructured":"Basagni S, Chlamtac I, Syrotiuk VR, Woodward BA (1998) A distance routing effect algorithm for mobility (dream). In: Proceedings 4th Conference on Mobile Computing and Networking (MOBICOM), ACM, New York, pp 76\u201384. https:\/\/doi.org\/10.1145\/288235.288254","DOI":"10.1145\/288235.288254"},{"key":"490_CR40","doi-asserted-by":"publisher","unstructured":"Singh A, Ramakrishnan CR, Smolka SA (2009) Query-based model checking of ad hoc network protocols. In: Proceedings 20th Conference on Concurrency Theory (CONCUR). LNCS, vol 5710. Springer, Heidelberg, pp 603\u2013619. https:\/\/doi.org\/10.1007\/978-3-642-04081-8_40","DOI":"10.1007\/978-3-642-04081-8_40"},{"issue":"3","key":"490_CR41","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s10703-016-0254-7","volume":"49","author":"F Ghassemi","year":"2016","unstructured":"Ghassemi F, Fokkink WJ (2016) Model checking mobile ad hoc networks. Formal Methods Syst Des 49(3):159\u2013189. https:\/\/doi.org\/10.1007\/s10703-016-0254-7","journal-title":"Formal Methods Syst Des"},{"issue":"2","key":"490_CR42","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1002\/spe.1021","volume":"41","author":"JF Groote","year":"2011","unstructured":"Groote JF, Keiren J, Stappers FPM, Wesselink W, Willemse TAC (2011) Experiences in developing the mCRL2 toolset. Softw Pract Exp 41(2):143\u2013153. https:\/\/doi.org\/10.1002\/spe.1021","journal-title":"Softw Pract Exp"},{"issue":"2","key":"490_CR43","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.ic.2009.10.003","volume":"208","author":"S Nanz","year":"2010","unstructured":"Nanz S, Nielson F, Nielson HR (2010) Static analysis of topology-dependent broadcast networks. Inf Comput 208(2):117\u2013139. https:\/\/doi.org\/10.1016\/j.ic.2009.10.003","journal-title":"Inf Comput"},{"key":"490_CR44","doi-asserted-by":"publisher","unstructured":"Namjoshi KS, Trefler RJ (2015) Analysis of dynamic process networks. In: Proceedings 21st Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol 9035. Springer, Heidelberg, pp 164\u2013178. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_11","DOI":"10.1007\/978-3-662-46681-0_11"},{"key":"490_CR45","doi-asserted-by":"publisher","unstructured":"Kojima H, Nagashima Y, Tsuchiya T (2016) Model checking techniques for state space reduction in MANET protocol verification. In: Proceedings IPDPS Workshop on Advances in Parallel and Distributed Computational Models, IEEE, New York, pp 509\u2013516. https:\/\/doi.org\/10.1109\/IPDPSW.2016.122","DOI":"10.1109\/IPDPSW.2016.122"},{"issue":"4","key":"490_CR46","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1016\/j.comcom.2007.10.031","volume":"31","author":"S Maag","year":"2008","unstructured":"Maag S, Grepet C, Cavalli AR (2008) A formal validation methodology for MANET routing protocols based on nodes\u2019 self similarity. Comput Commun 31(4):827\u2013841. https:\/\/doi.org\/10.1016\/j.comcom.2007.10.031","journal-title":"Comput Commun"},{"key":"490_CR47","doi-asserted-by":"publisher","unstructured":"Djouvas C, Griffeth ND, Lynch NA (2006) Testing self-similar networks. In: Proceedings 2nd Workshop on Model Based Testing (MBT). ENTCS, vol 164. Elsevier, Amsterdam, pp 67\u201382. https:\/\/doi.org\/10.1016\/j.entcs.2006.09.007","DOI":"10.1016\/j.entcs.2006.09.007"},{"key":"490_CR48","volume-title":"The dynamic source routing protocol (DSR) for mobile ad hoc networks for IPv4. RFC 4728. IETF","author":"Y-C Hu","year":"2007","unstructured":"Hu Y-C, Maltz DA, Johnson DB (2007) The dynamic source routing protocol (DSR) for mobile ad hoc networks for IPv4. RFC 4728. IETF. https:\/\/datatracker.ietf.org\/doc\/rfc4728\/"},{"key":"490_CR49","first-page":"139","volume-title":"Ad hoc networking","author":"DB Johnson","year":"2001","unstructured":"Johnson DB, Maltz DA, Broch J (2001) DSR: the dynamic source routing protocol for multi-hop wireless ad hoc networks. In: Ad hoc networking. Addison-Wesley, Boston, pp 139\u2013172. https:\/\/www.microsoft.com\/en-us\/research\/publication\/dsr-dynamic-source-routing-protocol-multi-hop-wireless-ad-hoc-networks\/"},{"issue":"4","key":"490_CR50","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0169-7552(89)90078-0","volume":"16","author":"F Belina","year":"1989","unstructured":"Belina F, Hogrefe D (1989) The CCITT-specification and description language SDL. Comput Netw ISDN Syst 16(4):311\u2013341. https:\/\/doi.org\/10.1016\/0169-7552(89)90078-0","journal-title":"Comput Netw ISDN Syst"},{"key":"490_CR51","doi-asserted-by":"publisher","unstructured":"Andr\u00e9s C, Maag S, Cavalli AR, Merayo MG, N\u00fa\u00f1ez M (2009) Analysis of the OLSR protocol by using formal passive testing. In: Proceedings 16th Asia-Pacific Software Engineering Conference (APSEC), IEEE, New York, pp 152\u2013159. https:\/\/doi.org\/10.1109\/APSEC.2009.37","DOI":"10.1109\/APSEC.2009.37"},{"key":"490_CR52","doi-asserted-by":"publisher","unstructured":"Lalanne F, Maag S (2013) Datamonitor - a formal approach for passively testing a MANET routing protocol. In: Proceedings 9th Wireless Communications and Mobile Computing Conference (IWCMC), IEEE, New York, pp 207\u2013212. https:\/\/doi.org\/10.1109\/IWCMC.2013.6583560","DOI":"10.1109\/IWCMC.2013.6583560"},{"key":"490_CR53","volume-title":"Routing information protocol. RFC 1058. IETF","author":"C Hedrick","year":"1988","unstructured":"Hedrick C (1988) Routing information protocol. RFC 1058. IETF. https:\/\/datatracker.ietf.org\/doc\/html\/rfc1058"},{"issue":"1\u20132","key":"490_CR54","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) Uppaal in a nutshell. Int J Softw Tools Technol Transf 1(1\u20132):134\u2013152. https:\/\/doi.org\/10.1007\/s100090050010","journal-title":"Int J Softw Tools Technol Transf"},{"key":"490_CR55","doi-asserted-by":"publisher","unstructured":"Wibling O, Parrow J, Pears AN (2005) Ad hoc routing protocol verification through broadcast abstraction. In: Proceedings 25th IFIP WG 6.1 Conference on Formal Techniques for Networked and Distributed Systems (FORTE). LNCS, vol 3731. Springer, Heidelberg, pp 128\u2013142. https:\/\/doi.org\/10.1007\/11562436_11","DOI":"10.1007\/11562436_11"},{"key":"490_CR56","doi-asserted-by":"publisher","unstructured":"Chiyangwa S, Kwiatkowska MZ (2005) A timing analysis of AODV. In: Proceedings 7th IFIP WG 6.1 Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). LNCS, vol 3535. Springer, Heidelberg, pp 306\u2013321. https:\/\/doi.org\/10.1007\/11494881_20","DOI":"10.1007\/11494881_20"},{"key":"490_CR57","doi-asserted-by":"publisher","unstructured":"Chaudhary K, Fehnker A, Mehta V (2017) Modelling, verification, and comparative performance analysis of the B.A.T.M.A.N. protocol. In: Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS@ETAPS). EPTCS, vol 244. pp 53\u201365. https:\/\/doi.org\/10.4204\/EPTCS.244.3","DOI":"10.4204\/EPTCS.244.3"},{"key":"490_CR58","unstructured":"Furlan D (2012) Improving B.A.T.M.A.N. routing stability and performance. Master\u2019s thesis, Universtit\u00e0 degli Studi di Trento. https:\/\/www.semanticscholar.org\/paper\/Improving-B.A.T.M.A.N.-Routing-Stability-and-Cigno-Furlan\/e73b1615721f5c2adb4d0f2129d10419b133e7f7"},{"key":"490_CR59","volume-title":"Better approach to mobile ad-hoc networking (B.A.T.M.A.N.). Draft. IETF","author":"A Neumann","year":"2008","unstructured":"Neumann A, Aichele C, Lindner M, Wunderlich S (2008) Better approach to mobile ad-hoc networking (B.A.T.M.A.N.). Draft. IETF. https:\/\/datatracker.ietf.org\/doc\/html\/draft-wunderlich-openmesh-manet-routing-00"},{"key":"490_CR60","doi-asserted-by":"publisher","unstructured":"Fehnker A, Chaudhary K, Mehta V (2018) An even better approach - improving the B.A.T.M.A.N. protocol through formal modelling and analysis. In: Proceedings 10th NASA Formal Methods Symposium (NFM). LNCS, vol 10811. Springer, Heidelberg, pp 164\u2013178. https:\/\/doi.org\/10.1007\/978-3-319-77935-5_12","DOI":"10.1007\/978-3-319-77935-5_12"},{"key":"490_CR61","doi-asserted-by":"publisher","unstructured":"Kamali M, H\u00f6fner P, Kamali M, Petre L (2015) Formal analysis of proactive, distributed routing. In: Proceedings 13th Conference on Software Engineering and Formal Methods (SEFM). LNCS, vol 9276. Springer, Heidelberg, pp 175\u2013189. https:\/\/doi.org\/10.1007\/978-3-319-22969-0_13","DOI":"10.1007\/978-3-319-22969-0_13"},{"key":"490_CR62","doi-asserted-by":"publisher","unstructured":"Kamali M, Petre L (2015) Improved recovery for proactive, distributed routing. In: Proceedings 20th Conference on Engineering of Complex Computer Systems (ICECCS), IEEE, New York, pp 178\u2013181. https:\/\/doi.org\/10.1109\/ICECCS.2015.27","DOI":"10.1109\/ICECCS.2015.27"},{"key":"490_CR63","doi-asserted-by":"publisher","unstructured":"Mouradian A, Aug\u00e9-Blum I (2014) Formal verification of real-time wireless sensor networks protocols: scaling up. In: Proceedings 26th Euromicro Conference on Real-Time Systems (ECRTS), IEEE, New York, pp 41\u201350. https:\/\/doi.org\/10.1109\/ECRTS.2014.12","DOI":"10.1109\/ECRTS.2014.12"},{"key":"490_CR64","doi-asserted-by":"publisher","unstructured":"Schmitt JB, Roedig U (2005) Sensor network calculus - a framework for worst case analysis. In: Proceedings 1st Conference in Distributed Computing in Sensor Systems (DCOSS). LNCS, vol 3560. Springer, Heidelberg, pp 141\u2013154. https:\/\/doi.org\/10.1007\/11502593_13","DOI":"10.1007\/11502593_13"},{"key":"490_CR65","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.comnet.2014.03.020","volume":"67","author":"A Mouradian","year":"2014","unstructured":"Mouradian A, Aug\u00e9-Blum I, Valois F (2014) RTXP: a localized real-time MAC-routing protocol for wireless sensor networks. Comput Networks 67:43\u201359. https:\/\/doi.org\/10.1016\/j.comnet.2014.03.020","journal-title":"Comput Networks"},{"key":"490_CR66","doi-asserted-by":"publisher","unstructured":"Hammal Y, Seddiki M, Bencha\u00efba M, Abdelli A (2017) Formal specification and analysis of a cross-layer overlay P2P construction protocol over MANETs. In: Proceedings 18th Wireless Communications and Networking Conference (WCNC), IEEE, New York, pp 1\u20136. https:\/\/doi.org\/10.1109\/WCNC.2017.7925622","DOI":"10.1109\/WCNC.2017.7925622"},{"key":"490_CR67","doi-asserted-by":"publisher","unstructured":"H\u00f6fner P, McIver A (2013) Statistical model checking of wireless mesh routing protocols. In: Proceedings 5th NASA Formal Methods Symposium (NFM). LNCS, vol 7871. Springer, Heidelberg, pp 322\u2013336. https:\/\/doi.org\/10.1007\/978-3-642-38088-4_22","DOI":"10.1007\/978-3-642-38088-4_22"},{"issue":"4","key":"490_CR68","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David A, Larsen KG, Legay A, Miku\u010dionis M, Poulsen DB (2015) Uppaal SMC tutorial. Int J Softw Tools Technol Transf 17(4):397\u2013415. https:\/\/doi.org\/10.1007\/s10009-014-0361-y","journal-title":"Int J Softw Tools Technol Transf"},{"key":"490_CR69","doi-asserted-by":"publisher","unstructured":"Dal Corso A, Macedonio D, Merro M (2015) Statistical model checking of ad hoc routing protocols in lossy grid networks. In: Proceedings 7th NASA Formal Methods Symposium (NFM). LNCS, vol 9058. Springer, Heidelberg, pp 112\u2013126. https:\/\/doi.org\/10.1007\/978-3-319-17524-9_9","DOI":"10.1007\/978-3-319-17524-9_9"},{"key":"490_CR70","doi-asserted-by":"publisher","unstructured":"Kamali M, Merro M, Dal Corso A (2018) AODVv2: performance vs. loop freedom. In: Proceedings 44th Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM). LNCS, vol 10706. Springer, Heidelberg, pp 337\u2013350. https:\/\/doi.org\/10.1007\/978-3-319-73117-9_24","DOI":"10.1007\/978-3-319-73117-9_24"},{"key":"490_CR71","doi-asserted-by":"publisher","unstructured":"Kamali M, Fehnker A (2018) Adaptive formal framework for WMN routing protocols. In: Proceedings 15th Conference on Formal Aspects of Component Software (FACS). LNCS, vol 11222. Springer, Heidelberg, pp 175\u2013195. https:\/\/doi.org\/10.1007\/978-3-030-02146-7_9","DOI":"10.1007\/978-3-030-02146-7_9"},{"issue":"2","key":"490_CR72","doi-asserted-by":"publisher","first-page":"162","DOI":"10.5121\/ijnsa.2010.2213","volume":"2","author":"U Herberg","year":"2010","unstructured":"Herberg U, Clausen TH (2010) Security issues in the optimized link state routing protocol version 2 (OLSRv2). Int J Netw Secur Appl 2(2):162\u2013181. https:\/\/doi.org\/10.5121\/ijnsa.2010.2213","journal-title":"Int J Netw Secur Appl"},{"issue":"1","key":"490_CR73","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"FJ Thayer","year":"1999","unstructured":"Thayer FJ, Herzog JC, Guttman JD (1999) Strand spaces: proving security protocols correct. J Comput Secur 7(1):191\u2013230. https:\/\/doi.org\/10.3233\/JCS-1999-72-304","journal-title":"J Comput Secur"},{"key":"490_CR74","doi-asserted-by":"publisher","unstructured":"Song DX (1999) Athena: a new efficient automatic checker for security protocol analysis. In: Proceedings 12th Computer Security Foundations Workshop (CSFW), IEEE, New York, pp 192\u2013202. https:\/\/doi.org\/10.1109\/CSFW.1999.779773","DOI":"10.1109\/CSFW.1999.779773"},{"key":"490_CR75","doi-asserted-by":"publisher","unstructured":"Yang S, Baras JS (2003) Modeling vulnerabilities of ad hoc routing protocols. In: Proceedings 1st Workshop on Security of Ad Hoc and Sensor Networks (SASN), ACM, New York, pp 12\u201320. https:\/\/doi.org\/10.1145\/986858.986861","DOI":"10.1145\/986858.986861"},{"issue":"1\u20132","key":"490_CR76","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s11276-004-4744-y","volume":"11","author":"Y Hu","year":"2005","unstructured":"Hu Y, Perrig A, Johnson DB (2005) Ariadne: a secure on-demand routing protocol for ad hoc networks. Wirel Networks 11(1\u20132):21\u201338. https:\/\/doi.org\/10.1007\/s11276-004-4744-y","journal-title":"Wirel Networks"},{"issue":"11","key":"490_CR77","doi-asserted-by":"publisher","first-page":"1533","DOI":"10.1109\/TMC.2006.170","volume":"5","author":"G \u00c1cs","year":"2006","unstructured":"\u00c1cs G, Butty\u00e1n L, Vajda I (2006) Provably secure on-demand source routing in mobile ad hoc networks. IEEE Trans Mob Comput 5(11):1533\u20131546. https:\/\/doi.org\/10.1109\/TMC.2006.170","journal-title":"IEEE Trans Mob Comput"},{"issue":"9","key":"490_CR78","doi-asserted-by":"publisher","first-page":"1180","DOI":"10.1109\/TMC.2009.13","volume":"8","author":"M Burmester","year":"2009","unstructured":"Burmester M, de Medeiros B (2009) On the security of route discovery in MANETs. IEEE Trans Mob Comput 8(9):1180\u20131188. https:\/\/doi.org\/10.1109\/TMC.2009.13","journal-title":"IEEE Trans Mob Comput"},{"key":"490_CR79","doi-asserted-by":"publisher","unstructured":"Benetti D, Merro M, Vigan\u00f2 L (2010) Model checking ad hoc network routing protocols: ARAN vs. endairA. In: Proceedings 8th Conference on Software Engineering and Formal Methods (SEFM), IEEE, New York, pp 191\u2013202. https:\/\/doi.org\/10.1109\/SEFM.2010.24","DOI":"10.1109\/SEFM.2010.24"},{"key":"490_CR80","doi-asserted-by":"publisher","unstructured":"Armando A, Basin DA, Boichut Y, Chevalier Y, Compagna L, Cu\u00e9llar J, Hankes Drielsma P, H\u00e9am P, Kouchnarenko O, Mantovani J, M\u00f6dersheim S, von Oheimb D, Rusinowitch M, Santiago J, Turuani M, Vigan\u00f2 L, Vigneron L (2005) The AVISPA tool for the automated validation of internet security protocols and applications. In: Proceedings 17th Conference on Computer Aided Verification (CAV). LNCS, vol 3576. Springer, Heidelberg, pp 281\u2013285. https:\/\/doi.org\/10.1007\/11513988_27","DOI":"10.1007\/11513988_27"},{"issue":"3","key":"490_CR81","doi-asserted-by":"publisher","first-page":"598","DOI":"10.1109\/JSAC.2004.842547","volume":"23","author":"K Sanzgiri","year":"2005","unstructured":"Sanzgiri K, LaFlamme D, Dahill B, Levine BN, Shields C, Belding-Royer EM (2005) Authenticated routing for ad hoc networks. IEEE J Sel Areas Commun 23(3):598\u2013610. https:\/\/doi.org\/10.1109\/JSAC.2004.842547","journal-title":"IEEE J Sel Areas Commun"},{"key":"490_CR82","unstructured":"Godskesen JC (2006) Formal verification of the ARAN protocol using the applied \u03c0-calculus. In: Proceedings 6th IFIP WG 1.7 Workshop on Issues in the Theory of Security (WITS). http:\/\/www.itu.dk\/jcg\/Papers\/ARAN-APPpi.pdf"},{"key":"490_CR83","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-319-10082-1_3","volume-title":"Foundations of security analysis and design vii (FOSAD), tutorial lectures. LNCS","author":"B Blanchet","year":"2013","unstructured":"Blanchet B (2013) Automatic verification of security protocols in the symbolic model: the verifier ProVerif. In: Foundations of security analysis and design VII (FOSAD), tutorial lectures. LNCS, vol 8604. Springer, Heidelberg, pp 54\u201387. https:\/\/doi.org\/10.1007\/978-3-319-10082-1_3"},{"key":"490_CR84","doi-asserted-by":"crossref","unstructured":"Pura M, Patriciu VV, Bica I (2009) Simulation of an identity-based cryptography scheme for ad hoc networks. In: Proceedings 6th Conference on Security and Cryptography (SECRYPT), INSTICC Press, Lisbon, pp 135\u2013139. https:\/\/www.naun.org\/main\/UPress\/cc\/19-311.pdf","DOI":"10.5220\/0002183701350139"},{"key":"490_CR85","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-662-48650-4_6","volume":"10","author":"M Pura","year":"2015","unstructured":"Pura M, Buchs D (2015) Symbolic model checking of security protocols for ad hoc networks on any topologies. Trans Petri Nets Other Model Concurr 10:109\u2013130. https:\/\/doi.org\/10.1007\/978-3-662-48650-4_6","journal-title":"Trans Petri Nets Other Model. Concurr."},{"issue":"3\u20134","key":"490_CR86","doi-asserted-by":"publisher","first-page":"229","DOI":"10.3233\/FI-2011-608","volume":"113","author":"S Hostettler","year":"2011","unstructured":"Hostettler S, Marechal A, Linard A, Risoldi M, Buchs D (2011) High-level petri net model checking with AlPiNA. Fundam Inform 113(3\u20134):229\u2013264. https:\/\/doi.org\/10.3233\/FI-2011-608","journal-title":"Fundam Inform"},{"key":"490_CR87","doi-asserted-by":"publisher","unstructured":"Sosnovich A, Grumberg O, Nakibly G (2013) Finding security vulnerabilities in a network protocol using parameterized systems. In: Proceedings 25th Conference on Computer Aided Verification (CAV). LNCS, vol 8044. Springer, Heidelberg, pp 724\u2013739. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_51","DOI":"10.1007\/978-3-642-39799-8_51"},{"key":"490_CR88","doi-asserted-by":"publisher","unstructured":"Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Proceedings 10th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol 2988. Springer, Heidelberg, pp 168\u2013176. https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"490_CR89","unstructured":"Nakibly G, Kirshon A, Gonikman D, Boneh D (2012) Persistent OSPF attacks. In: Proceedings 19th Network and Distributed System Security Symposium (NDSS), The Internet Society, Reston. https:\/\/www.ndss-symposium.org\/wp-content\/uploads\/2017\/09\/P01_3.pdf"},{"key":"490_CR90","doi-asserted-by":"publisher","unstructured":"Nakibly G, Sosnovich A, Menahem E, Waizel A, Elovici Y (2014) OSPF vulnerability to persistent poisoning attacks: a systematic analysis. In: Proceedings 30th Annual Computer Security Applications Conference (ACSAC), ACM, New York, pp 336\u2013345. https:\/\/doi.org\/10.1145\/2664243.2664278","DOI":"10.1145\/2664243.2664278"},{"key":"490_CR91","doi-asserted-by":"publisher","unstructured":"Darville C, H\u00f6fner P, Ivankovic F, Pam A (2022) Advanced models for the OSPF routing protocol. In: Proceedings 5th Workshop on Models for Formal Analysis of Real Systems (MARS@ETAPS). EPTCS, vol 355. pp 13\u201326. https:\/\/doi.org\/10.4204\/EPTCS.355.2","DOI":"10.4204\/EPTCS.355.2"},{"issue":"9","key":"490_CR92","doi-asserted-by":"publisher","first-page":"2032","DOI":"10.1016\/j.simpat.2011.05.008","volume":"19","author":"TR Andel","year":"2011","unstructured":"Andel TR, Back G, Yasinsac A (2011) Automating the security analysis process of secure ad hoc routing protocols. Simul Model Pract Theory 19(9):2032\u20132049. https:\/\/doi.org\/10.1016\/j.simpat.2011.05.008","journal-title":"Simul Model Pract Theory"},{"key":"490_CR93","doi-asserted-by":"crossref","unstructured":"Papadimitratos P, Haas ZJ (2002) Secure routing for mobile ad hoc networks. In: Proceedings SCS Communication Networks and Distributed Systems Modeling and Simulation Conference (CNDS), pp 1\u201313","DOI":"10.1016\/S1570-8705(03)00018-0"},{"key":"490_CR94","doi-asserted-by":"publisher","unstructured":"Cortier V, Degrieck J, Delaune S (2012) Analysing routing protocols: four nodes topologies are sufficient. In: Proceedings 1st Conference on Principles of Security and Trust (POST). LNCS, vol 7215. Springer, Heidelberg, pp 30\u201350. https:\/\/doi.org\/10.1007\/978-3-642-28641-4_3","DOI":"10.1007\/978-3-642-28641-4_3"},{"key":"490_CR95","doi-asserted-by":"publisher","unstructured":"Berton S, Yin H, Lin C, Min G (2006) Secure, disjoint, multipath source routing protocol (SDMSR) for mobile ad-hoc networks. In: Proceedings 5th Conference on Grid and Cooperative Computing (GCC), IEEE, New York. https:\/\/doi.org\/10.1109\/GCC.2006.86","DOI":"10.1109\/GCC.2006.86"},{"issue":"1\u20132","key":"490_CR96","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.tcs.2006.08.036","volume":"367","author":"S Nanz","year":"2006","unstructured":"Nanz S, Hankin C (2006) A framework for security analysis of mobile wireless networks. Theor Comput Sci 367(1\u20132):203\u2013227. https:\/\/doi.org\/10.1016\/j.tcs.2006.08.036","journal-title":"Theor Comput Sci"},{"key":"490_CR97","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1016\/j.ic.2014.07.004","volume":"238","author":"M Arnaud","year":"2014","unstructured":"Arnaud M, Cortier V, Delaune S (2014) Modeling and verifying ad hoc routing protocols. Inf Comput 238:30\u201367. https:\/\/doi.org\/10.1016\/j.ic.2014.07.004","journal-title":"Inf Comput"},{"key":"490_CR98","doi-asserted-by":"publisher","unstructured":"Godskesen JC (2007) A calculus for mobile ad hoc networks. In: Proceedings 9th Conference on Coordination Models and Languages (COORDINATION). LNCS, vol 4467. Springer, Heidelberg, pp 132\u2013150. https:\/\/doi.org\/10.1007\/978-3-540-72794-1_8","DOI":"10.1007\/978-3-540-72794-1_8"},{"key":"490_CR99","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/j.entcs.2009.06.018","volume-title":"Proceedings 15th Workshop on Expressiveness in Concurrency (express). ENTCS","author":"JC Godskesen","year":"2008","unstructured":"Godskesen JC (2008) A calculus for mobile ad-hoc networks with static location binding. In: Proceedings 15th Workshop on Expressiveness in Concurrency (express). ENTCS, vol 242. Elsevier, Amsterdam, pp 161\u2013183. https:\/\/doi.org\/10.1016\/j.entcs.2009.06.018"},{"issue":"2","key":"490_CR100","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/j.ic.2007.11.010","volume":"207","author":"M Merro","year":"2009","unstructured":"Merro M (2009) An observational theory for mobile ad hoc networks (full version). Inf Comput 207(2):194\u2013208. https:\/\/doi.org\/10.1016\/j.ic.2007.11.010","journal-title":"Inf Comput"},{"issue":"5","key":"490_CR101","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 (2013) A calculus of trustworthy ad hoc networks. Formal Aspects Comput 25(5):801\u2013832. https:\/\/doi.org\/10.1007\/s00165-011-0210-7","journal-title":"Formal Aspects Comput"},{"key":"490_CR102","doi-asserted-by":"publisher","unstructured":"Ghassemi F, Fokkink WJ, Movaghar A (2008) Restricted broadcast process theory. In: Proceedings 6th Conference on Software Engineering and Formal Methods (SEFM), IEEE, New York, pp 345\u2013354. https:\/\/doi.org\/10.1109\/SEFM.2008.25","DOI":"10.1109\/SEFM.2008.25"},{"issue":"4","key":"490_CR103","doi-asserted-by":"publisher","first-page":"375","DOI":"10.3233\/FI-2010-371","volume":"105","author":"F Ghassemi","year":"2010","unstructured":"Ghassemi F, Fokkink WJ, Movaghar A (2010) Equational reasoning on mobile ad hoc networks. Fundam Inform 105(4):375\u2013415. https:\/\/doi.org\/10.3233\/FI-2010-371","journal-title":"Fundam Inform"},{"issue":"28","key":"490_CR104","doi-asserted-by":"publisher","first-page":"3262","DOI":"10.1016\/j.tcs.2011.03.017","volume":"412","author":"F Ghassemi","year":"2011","unstructured":"Ghassemi F, Fokkink WJ, Movaghar A (2011) Verification of mobile ad hoc networks: an algebraic approach. Theor Comput Sci 412(28):3262\u20133282. https:\/\/doi.org\/10.1016\/j.tcs.2011.03.017","journal-title":"Theor Comput Sci"},{"issue":"1","key":"490_CR105","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/FI-2019-1775","volume":"165","author":"F Ghassemi","year":"2019","unstructured":"Ghassemi F, Fokkink WJ (2019) Reliable restricted process theory. Fundam Inform 165(1):1\u201341. https:\/\/doi.org\/10.3233\/FI-2019-1775","journal-title":"Fundam Inform"},{"key":"490_CR106","doi-asserted-by":"publisher","unstructured":"Kouzapas D, Philippou A (2011) A process calculus for dynamic networks. In: Proceedings Joint 13th IFIP WG 6.1 Conference on Formal Methods for Open Object-Based Distributed Systems and 31st IFIP WG 6.1 Conference on Formal Techniques for Distributed Systems (FMOODS\/FORTE). LNCS, vol 6722. Springer, Heidelberg, pp 213\u2013227. https:\/\/doi.org\/10.1007\/978-3-642-21461-5_14","DOI":"10.1007\/978-3-642-21461-5_14"},{"key":"490_CR107","doi-asserted-by":"publisher","unstructured":"Vasudevan S, Kurose JF, Towsley DF (2004) Design and analysis of a leader election algorithm for mobile ad hoc networks. In: Proceedings 12th Conference on Network Protocols (ICNP), IEEE, New York, pp 350\u2013360. https:\/\/doi.org\/10.1109\/ICNP.2004.1348124","DOI":"10.1109\/ICNP.2004.1348124"},{"key":"490_CR108","doi-asserted-by":"publisher","unstructured":"Ghassemi F, Talebi M, Movaghar A, Fokkink WJ (2011) Stochastic restricted broadcast process theory. In: Proceedings 8th European Performance Engineering Workshop (EPEW). LNCS, vol 6977. Springer, Heidelberg, pp 72\u201386. https:\/\/doi.org\/10.1007\/978-3-642-24749-1_7","DOI":"10.1007\/978-3-642-24749-1_7"},{"key":"490_CR109","doi-asserted-by":"publisher","unstructured":"Fehnker A, van Glabbeek RJ, H\u00f6fner P, McIver A, Portmann M, Tan WL (2012) A process algebra for wireless mesh networks. In: Proceedings 21st European Symposium on Programming (ESOP). LNCS, vol 7211. Springer, Heidelberg, pp 295\u2013315. https:\/\/doi.org\/10.1007\/978-3-642-28869-2_15","DOI":"10.1007\/978-3-642-28869-2_15"},{"key":"490_CR110","doi-asserted-by":"publisher","unstructured":"Fehnker A, van Glabbeek RJ, H\u00f6fner P, McIver A, Portmann M, Tan WL (2012) Automated analysis of AODV using UPPAAL. In: Proceedings 18th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol 7214. Springer, Heidelberg, pp 173\u2013187. https:\/\/doi.org\/10.1007\/978-3-642-28756-5_13","DOI":"10.1007\/978-3-642-28756-5_13"},{"key":"490_CR111","doi-asserted-by":"publisher","unstructured":"H\u00f6fner P, van Glabbeek RJ, Tan WL, Portmann M, McIver A, Fehnker A (2012) A rigorous analysis of AODV and its variants. In: Proceedings 15th Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM), ACM, New York, pp 203\u2013212. https:\/\/doi.org\/10.1145\/2387238.2387274","DOI":"10.1145\/2387238.2387274"},{"issue":"4","key":"490_CR112","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s00446-015-0262-7","volume":"29","author":"RJ van Glabbeek","year":"2016","unstructured":"van Glabbeek RJ, H\u00f6fner P, Portmann M, Tan WL (2016) Modelling and verifying the AODV routing protocol. Distrib Comput 29(4):279\u2013315. https:\/\/doi.org\/10.1007\/s00446-015-0262-7","journal-title":"Distrib Comput"},{"key":"490_CR113","doi-asserted-by":"publisher","unstructured":"Bourke T, van Glabbeek RJ, H\u00f6fner P (2014) A mechanized proof of loop freedom of the (untimed) AODV routing protocol. In: Proceedings 12th Symposium on Automated Technology for Verification and Analysis (ATVA). LNCS, vol 8837. Springer, Heidelberg, pp 47\u201363. https:\/\/doi.org\/10.1007\/978-3-319-11936-6_5","DOI":"10.1007\/978-3-319-11936-6_5"},{"key":"490_CR114","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"LNCS","author":"LC Paulson","year":"1994","unstructured":"Paulson LC (1994) Isabelle - a generic theorem prover. In: LNCS, vol 828. Springer, Heidelberg. https:\/\/doi.org\/10.1007\/BFb0030541"},{"issue":"3","key":"490_CR115","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s10817-015-9358-9","volume":"56","author":"T Bourke","year":"2016","unstructured":"Bourke T, van Glabbeek RJ, H\u00f6fner P (2016) Mechanizing a process algebra for network protocols. J Autom Reason 56(3):309\u2013341. https:\/\/doi.org\/10.1007\/s10817-015-9358-9","journal-title":"J Autom Reason"},{"key":"490_CR116","doi-asserted-by":"publisher","unstructured":"van Glabbeek RJ, H\u00f6fner P, van der Wal D (2018) Analysing AWN-specifications using mCRL2 (extended abstract). In: Proceedings 14th Conference on Integrated Formal Methods (IFM). LNCS, vol 11023. Springer, Heidelberg, pp 398\u2013418. https:\/\/doi.org\/10.1007\/978-3-319-98938-9_23","DOI":"10.1007\/978-3-319-98938-9_23"},{"key":"490_CR117","doi-asserted-by":"publisher","unstructured":"Bres E, van Glabbeek RJ, H\u00f6fner P (2016) A timed process algebra for wireless networks with an application in routing (extended abstract). In: Proceedings 25th European Symposium on Programming (ESOP). LNCS, vol 9632. Springer, Heidelberg, pp 95\u2013122. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_5","DOI":"10.1007\/978-3-662-49498-1_5"},{"key":"490_CR118","doi-asserted-by":"publisher","unstructured":"Barry R, van Glabbeek RJ, H\u00f6fner P (2020) Formalising the optimised link state routing protocol. In: Proceedings 4th Workshop on Models for Formal Analysis of Real Systems (MARS@ETAPS). EPTCS, vol 316. pp 40\u201371. https:\/\/doi.org\/10.4204\/EPTCS.316.3","DOI":"10.4204\/EPTCS.316.3"},{"key":"490_CR119","doi-asserted-by":"publisher","unstructured":"Drury J, H\u00f6fner P, Wang W (2020) Formal models of the OSPF routing protocol. In: Proceedings 4th Workshop on Models for Formal Analysis of Real Systems (MARS@ETAPS), vol 316. EPTCS, pp. 72\u2013120. https:\/\/doi.org\/10.4204\/EPTCS.316.4","DOI":"10.4204\/EPTCS.316.4"},{"issue":"19","key":"490_CR120","doi-asserted-by":"publisher","first-page":"1928","DOI":"10.1016\/j.tcs.2010.01.023","volume":"411","author":"I Lanese","year":"2010","unstructured":"Lanese I, Sangiorgi D (2010) An operational semantics for a calculus for wireless systems. Theor Comput Sci 411(19):1928\u20131948. https:\/\/doi.org\/10.1016\/j.tcs.2010.01.023","journal-title":"Theor Comput Sci"},{"key":"490_CR121","doi-asserted-by":"publisher","unstructured":"Wang M, Lu Y (2012) A timed calculus for mobile ad hoc networks. In: Proceedings 1st Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), vol 105. EPTCS, pp. 118\u2013134. https:\/\/doi.org\/10.4204\/EPTCS.105.9","DOI":"10.4204\/EPTCS.105.9"},{"issue":"9","key":"490_CR122","doi-asserted-by":"publisher","first-page":"1507","DOI":"10.1587\/TRANSINF.2022EDP7223","volume":"106","author":"N Chen","year":"2023","unstructured":"Chen N, Zhu H (2023) IoT modeling and verification: from the CaIT calculus to Uppaal. IEICE Trans Inf Syst 106(9):1507\u20131518. https:\/\/doi.org\/10.1587\/TRANSINF.2022EDP7223","journal-title":"IEICE Trans Inf Syst"},{"issue":"1","key":"490_CR123","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/J.IC.2018.01.001","volume":"259","author":"R Lanotte","year":"2018","unstructured":"Lanotte R, Merro M (2018) A semantic theory of the internet of things. Inf Comput 259(1):72\u2013101. https:\/\/doi.org\/10.1016\/J.IC.2018.01.001","journal-title":"Inf Comput"},{"issue":"1","key":"490_CR124","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner R, Parrow J, Walker D (1992) A calculus of mobile processes, I + II. Inf Comput 100(1):1\u201377. https:\/\/doi.org\/10.1016\/0890-5401(92)90008-4","journal-title":"Inf Comput"},{"issue":"1","key":"490_CR125","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(99)00231-5","volume":"240","author":"L Cardelli","year":"2000","unstructured":"Cardelli L, Gordon AD (2000) Mobile ambients. Theor Comput Sci 240(1):177\u2013213. https:\/\/doi.org\/10.1016\/S0304-3975(99)00231-5","journal-title":"Theor Comput Sci"},{"key":"490_CR126","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-47959-7_1","volume-title":"Proceedings ICCL workshop on internet programming languages. LNCS","author":"P Sewell","year":"1998","unstructured":"Sewell P, Wojciechowski PT, Pierce BC (1998) Location-independent communication for mobile agents: a two-level architecture. In: Proceedings ICCL workshop on internet programming languages. LNCS, vol 1686. Springer, Heidelberg, pp 1\u201331. https:\/\/doi.org\/10.1007\/3-540-47959-7_1"},{"issue":"4","key":"490_CR127","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/1734206.1734209","volume":"32","author":"P Sewell","year":"2010","unstructured":"Sewell P, Wojciechowski PT, Unyapoth A (2010) Nomadic pict: programming languages, communication infrastructure overlays, and semantics for mobile computation. ACM Trans Program Lang Syst 32(4):12\u201311263. https:\/\/doi.org\/10.1145\/1734206.1734209","journal-title":"ACM Trans Program Lang Syst"},{"key":"490_CR128","doi-asserted-by":"publisher","unstructured":"Ene C, Muntean T (2001) A broadcast-based calculus for communicating systems. In: Proceedings 6th IPDPS Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA), IEEE, New York. https:\/\/doi.org\/10.1109\/IPDPS.2001.925136","DOI":"10.1109\/IPDPS.2001.925136"},{"key":"490_CR129","doi-asserted-by":"publisher","unstructured":"Prasad KVS (2006) A prospectus for mobile broadcasting systems. In: Proceedings Workshop \u201cEssays on Algebraic Process Calculi\u201d (APC 25). ENTCS, vol 162. Elsevier, Amsterdam, pp 295\u2013300. https:\/\/doi.org\/10.1016\/j.entcs.2005.12.096","DOI":"10.1016\/j.entcs.2005.12.096"},{"issue":"6","key":"490_CR130","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1016\/j.scico.2009.07.008","volume":"75","author":"A Singh","year":"2010","unstructured":"Singh A, Ramakrishnan CR, Smolka SA (2010) A process calculus for mobile ad hoc networks. Sci Comput Program 75(6):440\u2013469. https:\/\/doi.org\/10.1016\/j.scico.2009.07.008","journal-title":"Sci Comput Program"},{"key":"490_CR131","doi-asserted-by":"publisher","unstructured":"Bengtson J, Johansson M, Parrow J, Victor B (2011) Psi-calculi: a framework for mobile processes with nominal data and logic. Log Methods Comput Sci 7(1). https:\/\/doi.org\/10.2168\/LMCS-7(1:11)2011","DOI":"10.2168\/LMCS-7(1:11)2011"},{"key":"490_CR132","doi-asserted-by":"publisher","unstructured":"Borgstr\u00f6m J, Huang S, Johansson M, Raabjerg P, Victor B, Pohjola J\u212b, Parrow J (2011) Broadcast psi-calculi with an application to wireless protocols. In: Proceedings 9th Conference on Software Engineering and Formal Methods (SEFM). LNCS, vol 7041. Springer, Heidelberg, pp 74\u201389. https:\/\/doi.org\/10.1007\/978-3-642-24690-6_7","DOI":"10.1007\/978-3-642-24690-6_7"},{"key":"490_CR133","doi-asserted-by":"publisher","unstructured":"Godskesen JC, H\u00fcttel H, K\u00fchnrich M (2009) Verification of correspondence assertions in a calculus for mobile ad hoc networks. In: Proceedings 7th Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA). ENTCS, vol 229. Elsevier, Amsterdam, pp 77\u201393. https:\/\/doi.org\/10.1016\/j.entcs.2009.06.030","DOI":"10.1016\/j.entcs.2009.06.030"},{"key":"490_CR134","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511611063","volume-title":"A distributed Pi-calculus","author":"MCB Hennessy","year":"2007","unstructured":"Hennessy MCB (2007) A distributed Pi-calculus. Cambridge University Press, Cambridge. https:\/\/doi.org\/10.1017\/CBO9780511611063"},{"key":"490_CR135","doi-asserted-by":"publisher","unstructured":"Abadi M, Gordon AD (1997) A calculus for cryptographic protocols: the spi calculus. In: Proceedings 4th Conference on Computer and Communications Security (CCS), ACM, New York, pp 36\u201347. https:\/\/doi.org\/10.1145\/266420.266432","DOI":"10.1145\/266420.266432"},{"key":"490_CR136","volume-title":"IP mobility support. RFC 2002. IETF","author":"CE Perkins","year":"1996","unstructured":"Perkins CE (1996) IP mobility support. RFC 2002. IETF. https:\/\/datatracker.ietf.org\/doc\/html\/rfc2002"},{"key":"490_CR137","doi-asserted-by":"publisher","unstructured":"Godskesen JC (2010) Observables for mobile and wireless broadcasting systems. In: Proceedings 12th Conference on Coordination Models and Languages (COORDINATION). LNCS, vol 6116. Springer, Heidelberg, pp 1\u201315. https:\/\/doi.org\/10.1007\/978-3-642-13414-2_1","DOI":"10.1007\/978-3-642-13414-2_1"},{"key":"490_CR138","doi-asserted-by":"publisher","unstructured":"Abadi M, Fournet C (2001) Mobile values, new names, and secure communication. In: Proceedings 28th Symposium on Principles of Programming Languages (POPL), ACM, New York, pp 104\u2013115. https:\/\/doi.org\/10.1145\/360204.360213","DOI":"10.1145\/360204.360213"},{"key":"490_CR139","doi-asserted-by":"publisher","unstructured":"Chr\u00e9tien R, Delaune S (2013) Formal analysis of privacy for routing protocols in mobile ad hoc networks. In: Proceedings 2nd Conference on Principles of Security and Trust (POST). LNCS, vol 7796. Springer, Heidelberg, pp 1\u201320. https:\/\/doi.org\/10.1007\/978-3-642-36830-1_1.","DOI":"10.1007\/978-3-642-36830-1_1"},{"key":"490_CR140","doi-asserted-by":"publisher","unstructured":"Kong J, Hong X (2003) ANODR: anonymous on demand routing with untraceable routes for mobile ad-hoc networks. In: Proceedings 4th Symposium on Mobile Ad Hoc Networking and Computing (MobiHoc), ACM, New York, pp 291\u2013302. https:\/\/doi.org\/10.1145\/778415.778449","DOI":"10.1145\/778415.778449"},{"issue":"2\u20133","key":"490_CR141","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0167-6423(95)00017-8","volume":"25","author":"KVS Prasad","year":"1995","unstructured":"Prasad KVS (1995) A calculus of broadcasting systems. Sci Comput Program 25(2\u20133):285\u2013327. https:\/\/doi.org\/10.1016\/0167-6423(95)00017-8","journal-title":"Sci Comput Program"},{"issue":"3","key":"490_CR142","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1145\/258077.258079","volume":"6","author":"G Roman","year":"1997","unstructured":"Roman G, McCann PJ, Plun JY (1997) Mobile unity: reasoning and specification in mobile computing. ACM Trans Softw Eng Methodol 6(3):250\u2013282. https:\/\/doi.org\/10.1145\/258077.258079","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"490_CR143","volume-title":"Parallel program design: a foundation","author":"KM Chandy","year":"1988","unstructured":"Chandy KM, Misra J (1988) Parallel program design: a foundation. Addison-Wesley, Boston"},{"key":"490_CR144","doi-asserted-by":"publisher","unstructured":"Smith G (2000) The object-Z specification language. Advances in formal methods, Kluwer, Alphen aan den Rijn. https:\/\/doi.org\/10.1007\/978-1-4615-5265-9","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"490_CR145","unstructured":"Smith G (2004) A framework for modelling and analysing mobile systems. In: Proceedings 27th Australasian Computer Science Conference (ACSC2004). CRPIT, vol 26. Australian Computer Society, Sydney, pp 193\u2013202. http:\/\/crpit.scem.westernsydney.edu.au\/abstracts\/CRPITV26Smith.html"},{"key":"490_CR146","doi-asserted-by":"publisher","unstructured":"Wu X, Sanders JW, Zhu H (2013) Formal modelling and analysis of AODV. In: Proceedings 18th Conference on Engineering of Complex Computer Systems (ICECCS), IEEE, New York, pp 93\u2013100. https:\/\/doi.org\/10.1109\/ICECCS.2013.22","DOI":"10.1109\/ICECCS.2013.22"},{"key":"490_CR147","doi-asserted-by":"publisher","unstructured":"Kamali M, Petre L (2016) Modelling link state routing in event-B. In: Proceedings 21st Conference on Engineering of Complex Computer Systems (ICECCS), IEEE, New York, pp 207\u2013210. https:\/\/doi.org\/10.1109\/ICECCS.2016.035","DOI":"10.1109\/ICECCS.2016.035"},{"key":"490_CR148","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in event-B: system an software design","author":"J-R Abrial","year":"2010","unstructured":"Abrial J-R (2010) Modeling in event-B: system an software design. Cambridge University Press, Cambridge. https:\/\/doi.org\/10.1017\/CBO9781139195881"},{"key":"490_CR149","doi-asserted-by":"publisher","unstructured":"Kamali M, Petre L (2017) Uppaal vs event-B for modelling optimised link state routing. In: Proceedings 11th Conference on Verification and Evaluation of Computer and Communication Systems (VECoS). LNCS, vol 10466. Springer, Heidelberg, pp 189\u2013203. https:\/\/doi.org\/10.1007\/978-3-319-66176-6_13","DOI":"10.1007\/978-3-319-66176-6_13"},{"key":"490_CR150","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-23509-7_16","volume-title":"Revised selected papers from software engineering, artificial intelligence, networking and Parallel\/Distributed computing (SNDP). Studies in computational intelligence","author":"F Fakhfakh","year":"2016","unstructured":"Fakhfakh F, Tounsi M, Kacem AH, Mosbah M (2016) Towards a formal model for dynamic networks through refinement and evolving graphs. In: Revised selected papers from software engineering, artificial intelligence, networking and Parallel\/Distributed computing (SNDP). Studies in computational intelligence, vol 612. Springer, Heidelberg, pp 227\u2013243. https:\/\/doi.org\/10.1007\/978-3-319-23509-7_16"},{"issue":"5","key":"490_CR151","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MNET.2004.1337732","volume":"18","author":"A Ferreira","year":"2004","unstructured":"Ferreira A (2004) Building a reference combinatorial model for MANETs. IEEE Netw 18(5):24\u201329. https:\/\/doi.org\/10.1109\/MNET.2004.1337732","journal-title":"IEEE Netw"},{"key":"490_CR152","first-page":"9","volume-title":"Specification and validation methods","author":"Y Gurevich","year":"1993","unstructured":"Gurevich Y (1993) Evolving algebras 1993: lipari guide. In: B\u00f6rger E (ed) Specification and validation methods. Oxford University Press, Oxford, pp 9\u201336. https:\/\/www.researchgate.net\/publication\/2241959_Evolving_Algebras_1993_Lipari_Guide"},{"key":"490_CR153","doi-asserted-by":"publisher","unstructured":"Bencz\u00far AA, Gl\u00e4sser U, Lukovszki T (2003) Formal description of a distributed location service for mobile ad hoc networks. In: Proceedings 10th Workshop on Abstract State Machines, Advances in Theory and Practice (ASM). LNCS, vol 2589. Springer, Heidelberg, pp 204\u2013217. https:\/\/doi.org\/10.1007\/3-540-36498-6_11","DOI":"10.1007\/3-540-36498-6_11"},{"issue":"2\u20133","key":"490_CR154","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/j.tcs.2004.11.009","volume":"336","author":"U Gl\u00e4sser","year":"2005","unstructured":"Gl\u00e4sser U, Gu Q (2005) Formal description and analysis of a distributed location service for mobile ad hoc networks. Theor Comput Sci 336(2\u20133):285\u2013309. https:\/\/doi.org\/10.1016\/j.tcs.2004.11.009","journal-title":"Theor Comput Sci"},{"key":"490_CR155","doi-asserted-by":"publisher","unstructured":"Gl\u00e4sser U, Prinz A (2005) ASM and SDL models of geographic routing in mobile ad hoc networks. In: Proceedings 12th SDL Forum. LNCS, vol 3530. Springer, Heidelberg, pp 162\u2013173. https:\/\/doi.org\/10.1007\/11506843_11","DOI":"10.1007\/11506843_11"},{"issue":"6","key":"490_CR156","doi-asserted-by":"publisher","first-page":"1310","DOI":"10.1109\/TCOM.1982.1095599","volume":"30","author":"A Rockstr\u00f6m","year":"1982","unstructured":"Rockstr\u00f6m A, Saracco R (1982) SDL-CCITT specification and description language. IEEE Trans Commun 30(6):1310\u20131318. https:\/\/doi.org\/10.1109\/TCOM.1982.1095599","journal-title":"IEEE Trans Commun"},{"key":"490_CR157","first-page":"29","volume":"1","author":"A Bianchi","year":"2014","unstructured":"Bianchi A, Pizzutilo S, Vessio G (2014) Suitability of abstract state machines for discussing mobile ad-hoc networks. Global J Adv Softw Eng 1:29\u201338. https:\/\/www.researchgate.net\/publication\/268813941_Suitability_of_Abstract_State_Machines_for_Discussing_Mobile_Ad-hoc_Networks","journal-title":"Global J Adv Softw Eng"},{"key":"490_CR158","doi-asserted-by":"publisher","unstructured":"Bianchi A, Pizzutilo S, Vessio G (2017) Intercepting blackhole attacks in MANETs: an ASM-based model. In: Proceedings 1st Workshop on Formal Approaches for Advanced Computing Systems (FAACS). LNCS, vol 10729. Springer, Heidelberg, pp 137\u2013152. https:\/\/doi.org\/10.1007\/978-3-319-74781-1_10","DOI":"10.1007\/978-3-319-74781-1_10"},{"key":"490_CR159","doi-asserted-by":"publisher","unstructured":"Hoffmann K, Mossakowski T (2002) Algebraic higher-order nets: graphs and Petri nets as tokens. In: Proceedings 16th Workshop on Recent Trends in Algebraic Development Techniques (WADT). LNCS, vol 2755. Springer, Heidelberg, pp 253\u2013267. https:\/\/doi.org\/10.1007\/978-3-540-40020-2_14","DOI":"10.1007\/978-3-540-40020-2_14"},{"issue":"1","key":"490_CR160","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1155\/2006\/704187","volume":"2","author":"P Bottoni","year":"2006","unstructured":"Bottoni P, De Rosa F, Hoffmann K, Mecella M (2006) Applying algebraic approaches for modeling workflows and their transformations in mobile networks. Mob Inf Syst 2(1):51\u201376. https:\/\/doi.org\/10.1155\/2006\/704187","journal-title":"Mob Inf Syst"},{"key":"490_CR161","doi-asserted-by":"publisher","unstructured":"Padberg J, Hoffmann K, Ehrig H, Modica T, Biermann E, Ermel C (2007) Maintaining consistency in layered architectures of mobile ad-hoc networks. In: Proceedings 10th Conference on Fundamental Approaches to Software Engineering (FASE). LNCS, vol 4422. Springer, Heidelberg, pp 383\u2013397. https:\/\/doi.org\/10.1007\/978-3-540-71289-3_29","DOI":"10.1007\/978-3-540-71289-3_29"},{"key":"490_CR162","doi-asserted-by":"publisher","unstructured":"Biermann E, Hoffmann K, Padberg J (2008) Layered architecture consistency for MANETs: introducing new team members. Electron Commun Eur Assoc Softw Sci Technol 12. https:\/\/doi.org\/10.14279\/tuj.eceasst.12.269","DOI":"10.14279\/tuj.eceasst.12.269"},{"issue":"6","key":"490_CR163","doi-asserted-by":"publisher","first-page":"1249","DOI":"10.1007\/s00165-021-00558-z","volume":"33","author":"B Archibald","year":"2021","unstructured":"Archibald B, Kulcs\u00e1r G, Sevegnani M (2021) A tale of two graph models: a case study in wireless sensor networks. Form Asp Comp 33(6):1249\u20131277. https:\/\/doi.org\/10.1007\/s00165-021-00558-z","journal-title":"Form Asp Comp"},{"key":"490_CR164","doi-asserted-by":"publisher","unstructured":"Ehrig H, Pfender M, Schneider HJ (1973) Graph-grammars: an algebraic approach. In: Proceedings 14th Symposium on Switching and Automata Theory, IEEE, New York, pp 167\u2013180. https:\/\/doi.org\/10.1109\/SWAT.1973.11","DOI":"10.1109\/SWAT.1973.11"},{"key":"490_CR165","doi-asserted-by":"publisher","unstructured":"Milner R (2001) Bigraphical reactive systems. In: Proceedings 12th Conference on Concurrency Theory (CONCUR). LNCS, vol 2154. Springer, Heidelberg, pp 16\u201335. https:\/\/doi.org\/10.1007\/3-540-44685-0_2","DOI":"10.1007\/3-540-44685-0_2"},{"issue":"3","key":"490_CR166","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/3685934","volume":"36","author":"M Albalwe","year":"2024","unstructured":"Albalwe M, Archibald B, Sevegnani M (2024) Modelling and analysing routing protocols diagrammatically with bigraphs. Formal Aspects Comput 36(3):17\u201311725. https:\/\/doi.org\/10.1145\/3685934","journal-title":"Formal Aspects Comput"},{"key":"490_CR167","volume-title":"RPL: IPv6 routing protocol for low-power and LossyNetworks. RFC 6550. IETF","author":"R Alexander","year":"2012","unstructured":"Alexander R, Brandt A, Vasseur JP, Hui J, Pister K, Thubert P, Levis P, Struik R, Kelsey R, Winter T (2012) RPL: IPv6 routing protocol for low-power and LossyNetworks. RFC 6550. IETF. https:\/\/www.rfc-editor.org\/info\/rfc6550"},{"key":"490_CR168","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1002\/wcm.72","volume":"2","author":"T Camp","year":"2002","unstructured":"Camp T, Boleng J, Davies V (2002) A survey of mobility models for ad hoc network research. Wirel Commun Mob Comput 2:483\u2013502. https:\/\/doi.org\/10.1002\/wcm.72","journal-title":"Wirel Commun Mob Comput"},{"issue":"7","key":"490_CR169","doi-asserted-by":"publisher","first-page":"884","DOI":"10.1006\/jpdc.2000.1718","volume":"61","author":"PA Patsouris","year":"2001","unstructured":"Patsouris PA (2001) Algebraic modeling of an ad hoc network for mobile computing. J Parallel Distrib Comput 61(7):884\u2013897. https:\/\/doi.org\/10.1006\/jpdc.2000.1718","journal-title":"J Parallel Distrib Comput"},{"key":"490_CR170","volume-title":"Modal theory: an algebraic approach to order, geometry, and convexity","author":"AB Romanowska","year":"1983","unstructured":"Romanowska AB, Smith JDH (1983) Modal theory: an algebraic approach to order, geometry, and convexity. Heldermann Verlag, Berlin"},{"issue":"2","key":"490_CR171","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1016\/j.jlap.2014.02.009","volume":"83","author":"P H\u00f6fner","year":"2014","unstructured":"H\u00f6fner P, McIver A (2014) Hopscotch - reaching the target hop by hop. J Log Algebraic Methods Program 83(2):212\u2013224. https:\/\/doi.org\/10.1016\/j.jlap.2014.02.009","journal-title":"J Log Algebraic Methods Program"},{"key":"490_CR172","doi-asserted-by":"publisher","unstructured":"Godskesen JC, Nanz S (2009) Mobility models and behavioural equivalence for wireless networks. In: Proceedings 11th Conference on Coordination Models and Languages (COORDINATION). LNCS, vol 5521. Springer, Heidelberg, pp 106\u2013122. https:\/\/doi.org\/10.1007\/978-3-642-02053-7_6","DOI":"10.1007\/978-3-642-02053-7_6"},{"key":"490_CR173","doi-asserted-by":"publisher","unstructured":"Wu X, Liu S, Zhu H, Zhao Y (2014) Reasoning about group-based mobility in MANETs. In: Proceedings 20th Pacific Rim Symposium on Dependable Computing, (PRDC), IEEE, New York, pp 244\u2013253. https:\/\/doi.org\/10.1109\/PRDC.2014.39","DOI":"10.1109\/PRDC.2014.39"},{"key":"490_CR174","doi-asserted-by":"publisher","unstructured":"Pei G, Gerla M, Hong X, Chiang C (1999) A wireless hierarchical routing protocol with group mobility. In: Proceedings Wireless Communications and Networking Conference, (WCNC), IEEE, New York, pp 1538\u20131542. https:\/\/doi.org\/10.1109\/WCNC.1999.796996","DOI":"10.1109\/WCNC.1999.796996"},{"key":"490_CR175","doi-asserted-by":"publisher","unstructured":"Song L, Godskesen JC (2010) Probabilistic mobility models for mobile and wireless networks. In: Proceedings 6th IFIP WG 2.2 Conference on Theoretical Computer Science (IFIP TCS). IFIP Advances in Information and Communication Technology, vol 323. Springer, Heidelberg, pp 86\u2013100. https:\/\/doi.org\/10.1007\/978-3-642-15240-5_7","DOI":"10.1007\/978-3-642-15240-5_7"},{"key":"490_CR176","doi-asserted-by":"crossref","unstructured":"Cheshire S, Aboba B, Guttman E (2005) Dynamic configuration of IPv4 link-local addresses. RFC 3927. IETF. https:\/\/datatracker.ietf.org\/doc\/html\/rfc3927","DOI":"10.17487\/rfc3927"},{"key":"490_CR177","doi-asserted-by":"publisher","unstructured":"Song L, Godskesen JC (2012) Broadcast abstraction in a stochastic calculus for mobile networks. In: Proceedings 7th IFIP WG 2.2 Conference on Theoretical Computer Science (IFIP TCS). LNCS, vol 7604. Springer, Heidelberg, pp 342\u2013356. https:\/\/doi.org\/10.1007\/978-3-642-33475-7_24","DOI":"10.1007\/978-3-642-33475-7_24"},{"key":"490_CR178","doi-asserted-by":"publisher","unstructured":"Ghassemi F, Movaghar A, Fokkink WJ (2010) Towards performance evaluation of mobile ad hoc network protocols. In: Proceedings 10th Conference on Application of Concurrency to System Design (ACSD), IEEE, New York, pp 85\u201392. https:\/\/doi.org\/10.1109\/ACSD.2010.20","DOI":"10.1109\/ACSD.2010.20"},{"key":"490_CR179","doi-asserted-by":"publisher","unstructured":"Hinton A, Kwiatkowska MZ, Norman G, Parker D (2006) Prism: a tool for automatic verification of probabilistic systems. In: Proceedings 12th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol 3920. Springer, Heidelberg, pp 441\u2013444. https:\/\/doi.org\/10.1007\/11691372_29","DOI":"10.1007\/11691372_29"},{"key":"490_CR180","doi-asserted-by":"publisher","unstructured":"Mouradian A, Aug\u00e9-Blum I (2013) Formal verification of real-time wireless sensor networks protocols with realistic radio links. In: Proceedings 21st Conference on Real-Time Networks and Systems (RTNS), ACM, New York, pp 213\u2013222. https:\/\/doi.org\/10.1145\/2516821.2516833","DOI":"10.1145\/2516821.2516833"},{"key":"490_CR181","doi-asserted-by":"publisher","unstructured":"Roedig U, Barroso AM, Sreenan CJ (2006) f-MAC: a deterministic media access control protocol without time synchronization. In: Proceedings 3rd European Workshop on Wireless Sensor Networks (EWSN). LNCS,, vol 3868. Springer, Heidelberg, pp 276\u2013291. https:\/\/doi.org\/10.1007\/11669463_21","DOI":"10.1007\/11669463_21"},{"key":"490_CR182","doi-asserted-by":"publisher","unstructured":"Kamali M, Katoen J (2020) Probabilistic model checking of AODV. In: Proceedings 17th Conference on Quantitative Evaluation of Systems (QEST). LNCS, vol 12289. Springer, Heidelberg, pp 54\u201373. https:\/\/doi.org\/10.1007\/978-3-030-59854-9_6","DOI":"10.1007\/978-3-030-59854-9_6"},{"issue":"10","key":"490_CR183","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp HC, D\u2019Argenio PR, Hermanns H, Katoen J (2006) Modest: a compositional modeling formalism for hard and softly timed systems. IEEE Trans Softw Eng 32(10):812\u2013830. https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans Softw Eng"},{"key":"490_CR184","doi-asserted-by":"publisher","unstructured":"Fehnker A, H\u00f6fner P, Kamali M, Mehta V (2013) Topology-based mobility models for wireless networks. In: Proceedings 10th Conference on Quantitative Evaluation of Systems (QEST). LNCS, vol 8054. Springer, Heidelberg, pp 389\u2013404. https:\/\/doi.org\/10.1007\/978-3-642-40196-1_32","DOI":"10.1007\/978-3-642-40196-1_32"},{"key":"490_CR185","unstructured":"van Hoesel LFW, Havinga PJM (2004) A lightweight medium access protocol (LMAC) for wireless sensor networks: reducing preamble transmissions and transceiver state switches. In: Proceedings 1st Workshop on Networked Sensing Systems (INSS), pp 205\u2013208. https:\/\/www.researchgate.net\/publication\/242150051_A_Lightweight_Medium_Access_Protocol_LMAC_for_Wireless_Sensor_Networks_Reducing_Preamble_Transmissions_and_Transceiver_State_Switches"},{"key":"490_CR186","doi-asserted-by":"publisher","unstructured":"Wu X, Zhu H (2015) A calculus for wireless sensor networks from quality perspective. In: Proceedings 16th Symposium on High Assurance Systems Engineering (HASE), IEEE, New York, pp 223\u2013231. https:\/\/doi.org\/10.1109\/HASE.2015.40","DOI":"10.1109\/HASE.2015.40"},{"key":"490_CR187","doi-asserted-by":"publisher","unstructured":"Wu X, Zhao Y, Zhu H (2016) Integrating a calculus with mobility and quality for wireless sensor networks. In: Proceedings 17th Symposium on High Assurance Systems Engineering (HASE), IEEE, New York, pp 220\u2013227. https:\/\/doi.org\/10.1109\/HASE.2016.29","DOI":"10.1109\/HASE.2016.29"},{"key":"490_CR188","doi-asserted-by":"publisher","unstructured":"Wu X, Zhu H, Xie W (2019) UTP semantics of a calculus for mobile ad hoc networks. In: Proceedings 7th Symposium on Unifying Theories of Programming (UTP). LNCS, vol 11885. Springer, Heidelberg, pp 198\u2013216. https:\/\/doi.org\/10.1007\/978-3-030-31038-7_10","DOI":"10.1007\/978-3-030-31038-7_10"},{"issue":"1","key":"490_CR189","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s11036-018-1142-8","volume":"24","author":"W Xie","year":"2019","unstructured":"Xie W, Zhu H, Wu X, Vinh PC (2019) Formal verification of mCWQ using extended Hoare logic. Mob Networks Appl 24(1):134\u2013144. https:\/\/doi.org\/10.1007\/s11036-018-1142-8","journal-title":"Mob Networks Appl"},{"issue":"10","key":"490_CR190","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580. https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"ACM"},{"issue":"1","key":"490_CR191","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1016\/j.jlamp.2015.05.002","volume":"85","author":"S Liu","year":"2016","unstructured":"Liu S, \u00d6lveczky PC, Meseguer J (2016) Modeling and analyzing mobile ad hoc networks in real-time maude. J Log Algebraic Methods Program 85(1):34\u201366. https:\/\/doi.org\/10.1016\/j.jlamp.2015.05.002","journal-title":"J Log Algebraic Methods Program"},{"key":"490_CR192","doi-asserted-by":"publisher","unstructured":"\u00d6lveczky PC, Meseguer J (2000) Real-Time Maude: a tool for simulating and analyzing real-time and hybrid systems. In: Proceedings 3rd Workshop on Rewriting Logic and Its Applications (WRLA). ENTCS, vol 36. Elsevier, Amsterdam, pp 361\u2013382. https:\/\/doi.org\/10.1016\/S1571-0661(05)80134-3","DOI":"10.1016\/S1571-0661(05)80134-3"},{"key":"490_CR193","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1016\/j.scico.2014.06.006","volume":"99","author":"D Lepri","year":"2015","unstructured":"Lepri D, \u00c1brah\u00e1m E, \u00d6lveczky PC (2015) Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Sci Comput Program 99:128\u2013192. https:\/\/doi.org\/10.1016\/j.scico.2014.06.006","journal-title":"Sci Comput Program"},{"issue":"2","key":"490_CR194","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s11235-015-0122-6","volume":"63","author":"L Gallina","year":"2016","unstructured":"Gallina L, Marin A, Rossi S (2016) Connectivity and energy-aware preorders for mobile ad-hoc networks. Telecommun Syst 63(2):307\u2013333. https:\/\/doi.org\/10.1007\/s11235-015-0122-6","journal-title":"Telecommun Syst"},{"key":"490_CR195","doi-asserted-by":"publisher","unstructured":"Gallina L, Marin A, Rossi S, Han T, Kwiatkowska MZ (2013) A process algebraic framework for estimating the energy consumption in ad-hoc wireless sensor networks. In: Proceedings 16th Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM), ACM, New York, pp 255\u2013262. https:\/\/doi.org\/10.1145\/2507924.2507958","DOI":"10.1145\/2507924.2507958"},{"issue":"3","key":"490_CR196","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1109\/TNET.2006.876186","volume":"14","author":"ZJ Haas","year":"2006","unstructured":"Haas ZJ, Halpern JY, Li L (2006) Gossip-based ad hoc routing. IEEE\/ACM Trans Netw 14(3):479\u2013491. https:\/\/doi.org\/10.1109\/TNET.2006.876186","journal-title":"IEEE\/ACM Trans Netw"},{"key":"490_CR197","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.peva.2013.11.003","volume":"73","author":"M Bugliesi","year":"2014","unstructured":"Bugliesi M, Gallina L, Hamadou S, Marin A, Rossi S (2014) Behavioural equivalences and interference metrics for mobile ad-hoc networks. Perform Evaluation 73:41\u201372. https:\/\/doi.org\/10.1016\/j.peva.2013.11.003","journal-title":"Perform Evaluation"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00490-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00490-5","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00490-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T09:11:54Z","timestamp":1772788314000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00490-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12,15]]},"references-count":197,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,2]]}},"alternative-id":["490"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00490-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,12,15]]},"assertion":[{"value":"23 December 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 October 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"1"}}