Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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–270
Rebeca formal modeling language. http://www.rebeca-lang.org/wiki/pmwiki.php/Tools/Afra
Agha GA (1990) ACTORS—a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence. MIT Press, Cambridge, MA
Bertsekas DP, Gallager RG (1992) Data networks. Prentice Hall, Upper Saddle River, NJ
Borgström J, Huang S, Johansson M, Raabjerg P, Victor B, Pohjola JÅ, Parrow J (2015) Broadcast psi-calculi with an application to wireless protocols. Softw Syst Model 14(1): 201–216
Basler Gérard, Mazzucchi Michele, Wahl Thomas, Kroening Daniel (2009) Symbolic counter abstraction for concurrent software. In Computer Aided Verification, Springer pp 64–78
Bhargavan K, Obradovic D, Gunter CA (2002) Formal verification of standards for distance vector routing protocols. J ACM 49(4): 538–576
Cui T, Chen L, Ho T (2007) Distributed optimization in wireless networks using broadcast advantage. In: Decision and control. IEEE, pp 5839–5844
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–158
Dechter R, Kleinrock L (1986) Broadcast communications and distributed algorithms. IEEE Trans Comput 35(3): 210–219
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–1182
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–300
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–65
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–419
Ene C, Muntean T (1999) Expressiveness of point-to-point versus broadcast communications. In: Ciobanu G, Păun G (eds) Fundamentals of computation theory. FCT 1999, volume 1684 of LNCS. Springer, Berlin
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–156
Fehnker A, van Glabbeek R, Höfner 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–187
Fehnker A, Van Glabbeek R, Höfner 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
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–232
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–354
Ghassemi F, Fokkink W, Movaghar A (2011) Verification of mobile ad hoc networks: an algebraic approach. Theor Comput Sci 412(28): 3262–3282
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–150
Godskesen JC (2009) A calculus for mobile ad-hoc networks with static location binding. Electr Notes Theor Comput Sci 242(1): 161–183
Godskesen JC (2010) Observables for mobile and wireless broadcasting systems. In: Coordination models and languages, volume 6116 of LNCS. Springer, Berlin, pp 1–15
Hewitt C (1977) Viewing control structures as patterns of passing messages. Artif Intell 8(3): 323–364
Jaghoori MM, Sirjani M, Mousavi MR, Khamespanah E, Movaghar A (2010) Symmetry and partial order reduction techniques in model checking Rebeca. Acta Inform 47(1): 33–66
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–14
Kuhn F, Lynch NA, Newport CC (2011) The abstract MAC layer. Distrib Comput 24(3–4): 187–206
Khamespanah E, Sirjani M, Sabahi-Kaviani Z, Khosravi R, Izadi M (2015) Timed rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Sci Comput Program 98: 184–204
Merro M (2009) An observational theory for mobile ad hoc networks (full version). Inf Comput 207(2):194–208, Special issue on Structural Operational Semantics (SOS)
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–270
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
Mateescu R, Sighireanu M (2003) Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci Comput Program 46(3): 255–281
Mezzetti N, Sangiorgi D (2006) Towards a calculus for wireless systems. Electr Notes Theor Comput Sci 158(0): 331–353
Nanz S, Hankin C (2006) A framework for security analysis of mobile wireless networks. Theor Comput Sci 367(1–2): 203–227
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–178
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–112
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–100
Pohjola JÅ, Borgström J, Parrow J, Raabjerg P (2013) Negative premises in applied process calculi. Technical report, Department of Information Technology, Uppsala University
Peng J (2008) A new arq scheme for reliable broadcasting in wireless lans. IEEE Commun Lett 12(2): 146–148
Plotkin GD (1981) A structural approach to operational semantics. Technical Report DAIMI FN-19, University of Aarhus
Pnueli A, Xu J, Zuck LD (2002) Liveness with (0, 1, infty)-counter abstraction. In: 14th international conference on computer aided verification, CAV ’02, Springer, pp 107–122
Reynisson AH, Sirjani M, Aceto L, Cimini M, Jafari A, Ingólfsdóttir A, Sigurdarson SH (2014) Modelling and simulation of asynchronous real-time systems using Timed Rebeca. Sci Comput Program 89:41–68
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–56
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–65
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–501
Sirjani M, Movaghar A, Shali A, de Boer FS (2004) Modeling and verification of reactive systems using Rebeca. Fundam Inform 63(4): 385–410
Singh A, Ramakrishnan CR, Smolka SA (2010) A process calculus for mobile ad hoc networks. Sci Comput Program 75(6): 440–469
Sabouri H, Sirjani M (2010) Slicing-based reductions for rebeca. Electr Notes Theor Comput Sci 260: 209–224
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–32
van Glabbeek RJ, Höfner P, Portmann M, Tan WL (2016) Modelling and verifying the AODV routing protocol. Distrib Comput 29(4): 279–315
van Glabbeek R, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3): 555–600
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–150
Wibling O, Parrow J, Pears A (2004) Automatized verification of ad hoc routing protocols. In: de Frutos-Escrig D, Núñez M (eds) Formal techniques for networked and distributed systems, volume 3235 of LNCS. Springer, Berlin, pp 343–358
Wibling O, Parrow J, Pears A (2005) Ad hoc routing protocol verification through broadcast abstraction. In: Wang F (ed) Formal techniques for networked and distributed systems-FORTE 2005. Springer, Berlin, pp 128–142
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–128
Author information
Authors and Affiliations
Corresponding author
Additional information
Joachim Parrow
Electronic Supplementary Material
The Below is the Electronic Supplementary Material.
Rights and permissions
About this article
Cite this article
Yousefi, B., Ghassemi, F. & Khosravi, R. Modeling and efficient verification of wireless ad hoc networks. Form Asp Comp 29, 1051–1086 (2017). https://doi.org/10.1007/s00165-017-0429-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-017-0429-z