{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:28:23Z","timestamp":1772836103566,"version":"3.50.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,11,1]],"date-time":"2017-11-01T00:00:00Z","timestamp":1509494400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Wireless ad hoc networks, in particular mobile ad hoc networks (MANETs), are growing very fast as they make communication easier and more available. However, their protocols tend to be difficult to design due to topology dependent behavior of wireless communication, and their distributed and adaptive operations to topology dynamism. Therefore, it is desirable to have them modeled and verified using formal methods. In this paper, we present an actor-based modeling language with the aim to model MANETs. We address main challenges of modeling wireless ad hoc networks such as local broadcast, underlying topology, and its changes, and discuss how they can be efficiently modeled at the semantic level to make their verification amenable. The new framework abstracts the data link layer services by providing asynchronous (local) broadcast and unicast communication, while message delivery is in order and is guaranteed for connected receivers. We illustrate the applicability of our framework through two routing protocols, namely flooding and AODVv2-11, and show how efficiently their state spaces can be reduced by the proposed techniques. Furthermore, we demonstrate a loop formation scenario in AODV, found by our analysis tool.<\/jats:p>","DOI":"10.1007\/s00165-017-0429-z","type":"journal-article","created":{"date-parts":[[2017,4,19]],"date-time":"2017-04-19T19:16:24Z","timestamp":1492629384000},"page":"1051-1086","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Modeling and efficient verification of wireless ad hoc networks"],"prefix":"10.1145","volume":"29","author":[{"given":"Behnaz","family":"Yousefi","sequence":"first","affiliation":[{"name":"School of Electrical and Computer Engineering, University of Tehran, N. Kargar Ave., Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fatemeh","family":"Ghassemi","sequence":"additional","affiliation":[{"name":"School of Electrical and Computer Engineering, University of Tehran, N. Kargar Ave., Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramtin","family":"Khosravi","sequence":"additional","affiliation":[{"name":"School of Electrical and Computer Engineering, University of Tehran, N. Kargar Ave., Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abdulla PA Delzanno G Rezine O Sangnier A Traverso R (2011) On the verification of timed ad hoc networks. In: 9th international conference on formal modeling and analysis of timed systems volume 6919 of LNCS Springer pp 256\u2013270","DOI":"10.1007\/978-3-642-24310-3_18"},{"key":"e_1_2_1_2_2_2","unstructured":"Rebeca formal modeling language. http:\/\/www.rebeca-lang.org\/wiki\/pmwiki.php\/Tools\/Afra"},{"key":"e_1_2_1_2_3_2","unstructured":"Agha GA (1990) ACTORS\u2014a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence. MIT Press Cambridge MA"},{"key":"e_1_2_1_2_4_2","unstructured":"Bertsekas DP Gallager RG (1992) Data networks. Prentice Hall Upper Saddle River NJ"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-013-0375-z"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Basler G\u00e9rard Mazzucchi Michele Wahl Thomas Kroening Daniel (2009) Symbolic counter abstraction for concurrent software. In Computer Aided Verification Springer pp 64\u201378","DOI":"10.1007\/978-3-642-02658-4_9"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"e_1_2_1_2_8_2","unstructured":"Cui T Chen L Ho T (2007) Distributed optimization in wireless networks using broadcast advantage. In: Decision and control. IEEE pp 5839\u20135844"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Clarke EM Emerson EA Jha S Sistla AP (1998) Symmetry reductions in model checking. In: Hu AJ Vardi MY (eds) Computer aided verification. Springer Berlin pp 147\u2013158","DOI":"10.1007\/BFb0028741"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676745"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"De Renesse R Aghvami AH (2004) Formal verification of ad-hoc routing protocols using spin model checker. In 12th IEEE mediterranean electrotechnical conference volume 3. IEEE pp 1177\u20131182","DOI":"10.1109\/MELCON.2004.1348275"},{"key":"e_1_2_1_2_12_2","unstructured":"Delzanno G Sangnier A Traverso R Zavattaro G (2012) On the complexity of parameterized reachability in reconfigurable broadcast networks. In: Annual conference on foundations of software technology and theoretical computer science volume 18 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik pp 289\u2013300"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Delzanno G Sangnier A Zavattaro G (2011) Parameterized verification of safety properties in ad hoc network protocols. In: First international workshop on process algebra and coordination volume 60 of EPTCS pp 56\u201365","DOI":"10.4204\/EPTCS.60.4"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"De Nicola R Vaandrager FW (1990) Action versus state based logics for transition systems. In: Semantics of systems of concurrent processes volume 469 of Lecture notes in computer science. Springer pp 407\u2013419","DOI":"10.1007\/3-540-53479-2_17"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Ene C Muntean T (1999) Expressiveness of point-to-point versus broadcast communications. In: Ciobanu G P\u0103un G (eds) Fundamentals of computation theory. FCT 1999 volume 1684 of LNCS. Springer Berlin","DOI":"10.1007\/3-540-48321-7_21"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Emerson EA Trefler RJ (1999) From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Pierre L Kropf T (eds) Correct hardware design and verification methods. Springer Berlin pp 142\u2013156","DOI":"10.1007\/3-540-48153-2_12"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Fehnker A van Glabbeek R H\u00f6fner P McIver A Portmann M Tan WL (2012) Automated analysis of AODV using Uppaal. In: Tools and algorithms for the construction and analysis of systems volume 7214 of LNCS. Springer Berlin pp 173\u2013187","DOI":"10.1007\/978-3-642-28756-5_13"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Fehnker A Van Glabbeek R H\u00f6fner P McIver A Portmann M Tan WL (2013) A process algebra for wireless mesh networks used for modelling verifying and analysing AODV. arXiv preprint arXiv:1312.7645","DOI":"10.1007\/978-3-642-28869-2_15"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Ghassemi F Ahmadi S Fokkink W Movaghar A (2013) Model checking MANETs with arbitrary mobility. In: Arbab F Sirjani M (eds) Fundamentals of software engineering. Springer Berlin pp 217\u2013232","DOI":"10.1007\/978-3-642-40213-5_14"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Ghassemi F Fokkink W Movaghar A (2008) Restricted broadcast process theory. In: Sixth IEEE international conference on software engineering and formal methods (SEFM). IEEE Computer Society pp 345\u2013354","DOI":"10.1109\/SEFM.2008.25"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.03.017"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Godskesen JC (2007) A calculus for mobile ad hoc networks. In: Murphy AL Vitek J (eds) Coordination models and languages volume 4467 of LNCS. Springer Berlin pp 132\u2013150","DOI":"10.1007\/978-3-540-72794-1_8"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.06.018"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Godskesen JC (2010) Observables for mobile and wireless broadcasting systems. In: Coordination models and languages volume 6116 of LNCS. Springer Berlin pp 1\u201315","DOI":"10.1007\/978-3-642-13414-2_1"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(77)90033-9"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-009-0111-x"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Katoen J-P (2011) Model checking: one can do much more than you think! In: Arbab F Sirjani M (eds) Fundamentals of software engineering. Springer Berlin pp 1\u201314","DOI":"10.1007\/978-3-642-29320-7_1"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-010-0118-0"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.07.005"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Merro M (2009) An observational theory for mobile ad hoc networks (full version). Inf Comput 207(2):194\u2013208 Special issue on Structural Operational Semantics (SOS)","DOI":"10.1016\/j.ic.2007.11.010"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Mclver AK Fehnker A (2006) Formal techniques for the analysis of wireless networks. In: Second international symposium on leveraging applications of formal methods verification and validation. IEEE pp 263\u2013270","DOI":"10.1109\/ISoLA.2006.51"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Mahmud SA Khan S Khan S Al-Raweshidy H (2006) A comparison of manets and wmns: commercial feasibility of community wireless networks and manets. In: 1st international conference on access networks. ACM","DOI":"10.1145\/1189355.1189373"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00094-1"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.017"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.036"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Namjoshi KS Trefler RJ (2015a) Analysis of dynamic process networks. In: Baier C Tinelli C (eds) Tools and algorithms for the construction and analysis of systems volume 9035 of LNCS. Springer Berlin pp 164\u2013178","DOI":"10.1007\/978-3-662-46681-0_11"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Namjoshi KS Trefler RJ (2015b) Loop freedom in aodvv2. In: Graf S Viswanathan M (eds) Formal techniques for distributed objects components and systems volume 9039 of LNCS. Springer Cham pp 98\u2013112","DOI":"10.1007\/978-3-319-19195-9_7"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Perkins CE Belding-Royer EM (1999) Ad-hoc on-demand distance vector routing. In: 2nd workshop on mobile computing systems and applications. IEEE Computer Society Washington DC pp 90\u2013100","DOI":"10.1109\/MCSA.1999.749281"},{"key":"e_1_2_1_2_39_2","unstructured":"Pohjola J\u00c5 Borgstr\u00f6m J Parrow J Raabjerg P (2013) Negative premises in applied process calculi. Technical report Department of Information Technology Uppsala University"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/LCOMM.2008.071275"},{"key":"e_1_2_1_2_41_2","unstructured":"Plotkin GD (1981) A structural approach to operational semantics. Technical Report DAIMI FN-19 University of Aarhus"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Pnueli A Xu J Zuck LD (2002) Liveness with (0 1 infty)-counter abstraction. In: 14th international conference on computer aided verification CAV \u201902 Springer pp 107\u2013122","DOI":"10.1007\/3-540-45657-0_9"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Reynisson AH Sirjani M Aceto L Cimini M Jafari A Ing\u00f3lfsd\u00f3ttir A Sigurdarson SH (2014) Modelling and simulation of asynchronous real-time systems using Timed Rebeca. Sci Comput Program 89:41\u201368","DOI":"10.1016\/j.scico.2014.01.008"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Sirjani M Jaghoori MM (2011) Ten years of analyzing actors: Rebeca experience. In: Agha G Meseguer J Danvy O (eds) Formal modeling: actors open systems biological systems. Springer Berlin pp 20\u201356","DOI":"10.1007\/978-3-642-24933-4_3"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Sabouri H Khosravi R (2013) Delta modeling and model checking of product families. In: Arbab F Sirjani M (eds) Fundamentals of software engineering. Springer Berlin pp 51\u201365","DOI":"10.1007\/978-3-642-40213-5_4"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Si W Li C (2004) RMAC: A reliable multicast MAC protocol for wireless ad hoc networks. In: 33rd international conference on parallel processing (ICPP 2004). IEEE Computer Society pp 494\u2013501","DOI":"10.1109\/ICPP.2004.1327959"},{"issue":"4","key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","first-page":"385","DOI":"10.3233\/FUN-2004-63405","article-title":"Modeling and verification of reactive systems using Rebeca","volume":"63","author":"Sirjani M","year":"2004","journal-title":"Fundam Inform"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2009.07.008"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.12.039"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Saksena M Wibling O Jonsson B (2008) Graph grammar modeling and verification of ad hoc routing protocols. In: 14th international conference on tools and algorithms for the construction and analysis of systems volume 4963 of LNCS. Springer pp 18\u201332","DOI":"10.1007\/978-3-540-78800-3_3"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-015-0262-7"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/233551.233556"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Varshosaz M Khosravi R (2012) Modeling and verification of probabilistic actor systems using pRebeca. In: Aoki T Taguchi K (eds) Formal methods and software engineering. Springer Berlin pp 135\u2013150","DOI":"10.1007\/978-3-642-34281-3_12"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Wibling O Parrow J Pears A (2004) Automatized verification of ad hoc routing protocols. In: de Frutos-Escrig D N\u00fa\u00f1ez M (eds) Formal techniques for networked and distributed systems volume 3235 of LNCS. Springer Berlin pp 343\u2013358","DOI":"10.1007\/978-3-540-30232-2_22"},{"key":"#cr-split#-e_1_2_1_2_55_2.1","doi-asserted-by":"crossref","unstructured":"Wibling O Parrow J Pears A (2005) Ad hoc routing protocol verification through broadcast abstraction. In: Wang F","DOI":"10.1007\/11562436_11"},{"key":"#cr-split#-e_1_2_1_2_55_2.2","unstructured":"(ed) Formal techniques for networked and distributed systems-FORTE 2005. Springer Berlin pp 128-142"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Yousefi B Ghassemi F Khosravi R (2015) Modeling and efficient verification of broadcasting actors. In: In pre-proceeding of 6th IPM international conference on fundamentals of software engineering pp 114\u2013128","DOI":"10.1007\/978-3-319-24644-4_5"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0429-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0429-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0429-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0429-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:12:41Z","timestamp":1750201961000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0429-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":57,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["10.1007\/s00165-017-0429-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0429-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11]]}}}