Abstract
Wireless Mesh Networks (WMNs) are self-organising and self-healing wireless networks that provide support for broadband communication without requiring fixed infrastructure. A determining factor for the performance and reliability of such networks is the routing protocols applied in these networks. Formal modelling and verification of routing protocols are challenging tasks, often skipped by protocol designers. Despite some commonality between different models of routing protocols that have been published, these models are often tailored to a specific protocol which precludes easily comparing models. This paper presents an adaptive, generic and reusable framework as well as crucial generic properties w.r.t. system requirements, to model and verify WMN routing protocols. In this way, protocol designers can adapt the generic models based on protocol specifications and verify routing protocols prior to implementation. This model uses Uppaal SMC to identify the main common components of routing protocols, capturing timing aspect of protocols, communication between nodes, probabilities of message loss and link breakage, etc.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
To avoid confusion, we will refer to this type of communication as multicast, instead of broadcast. We reserve the term broadcast for Uppaal channels.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7
Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538–576 (2002)
Chaudhary, K., Fehnker, A., Mehta, V.: Modelling, verification, and comparative performance analysis of the B.A.T.M.A.N. protocol. In: Hermanns, H., Höfner, P. (eds.) MARS 2017, vol. 244, pp. 53–65 (2017)
Clausen, T., Jacquet, P.: Optimized link state routing protocol (OLSR). RFC3626 (2003). http://www.ietf.org/rfc/rfc3626
Dal Corso, A., Macedonio, D., Merro, M.: Statistical model checking of ad hoc routing protocols in lossy grid networks. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 112–126. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_9
David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. STTT 17(4), 397–415 (2015)
Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 173–187. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_13
Fehnker, A., van Hoesel, L., Mader, A.: Modelling and verification of the LMAC protocol for wireless sensor networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 253–272. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73210-5_14
Fehnker, A., Höfner, P., Kamali, M., Mehta, V.: Topology-based mobility models for wireless networks. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 389–404. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40196-1_32
van Glabbeek, R., Höfner, P., Portmann, M., Tan, W.L.: Modelling and verifying the AODV routing protocol. Distrib. Comput. 29(4), 279–315 (2016)
Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 73–84. Springer, Berlin (2004)
Höfner, P., McIver, A.: Statistical model checking of wireless mesh routing protocols. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 322–336. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38088-4_22
Kamali, M., Petre, L.: Modelling link state routing in event-B. In: Wang, H., Mokhtari, M. (eds.) ICECCS 2016, pp. 207–210. IEEE (2016)
Kamali, M., Höfner, P., Kamali, M., Petre, L.: Formal analysis of proactive, distributed routing. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 175–189. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22969-0_13
Kamali, M., Merro, M., Dal Corso, A.: AODVv2: performance vs. loop freedom. In: Tjoa, A.M., Bellatreche, L., Biffl, S., van Leeuwen, J., Wiedermann, J. (eds.) SOFSEM 2018. LNCS, vol. 10706, pp. 337–350. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73117-9_24
Kamali, M., Petre, L.: Improved recovery for proactive, distributed routing. In: ICECCS 2015, pp. 178–181. IEEE (2015)
Liu, S., Ölveczky, P.C., Meseguer, J.: A framework for mobile ad hoc networks in real-time maude. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 162–177. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12904-4_9
Neumann, A., Aichele, C., Lindner, M., Wunderlich, S.: Better approach to mobile ad-hoc networking (BATMAN). Internet draft00 (2008). https://tools.ietf.org/html/draft-wunderlich-openmesh-manet-routing-00
Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. High.-Order Symb. Comput. 20(1), 161–196 (2007)
Perkins, C., Stan, R., Dowdell, J., Steenbrink, L., Mercieca, V.: Ad hoc on-demand distance vector version 2 (AODVv2) routing. Internet Draft 16 (2016). https://datatracker.ietf.org/doc/draft-ietf-manet-aodvv2
Yousefi, B., Ghassemi, F., Khosravi, R.: Modeling and efficient verification of wireless ad hoc networks. Form. Asp. Comput. 29(6), 1051–1086 (2017)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Kamali, M., Fehnker, A. (2018). Adaptive Formal Framework for WMN Routing Protocols. In: Bae, K., Ölveczky, P. (eds) Formal Aspects of Component Software. FACS 2018. Lecture Notes in Computer Science(), vol 11222. Springer, Cham. https://doi.org/10.1007/978-3-030-02146-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-02146-7_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02145-0
Online ISBN: 978-3-030-02146-7
eBook Packages: Computer ScienceComputer Science (R0)