Abstract
This paper presents an incremental formal development of the Dynamic Source Routing (DSR) protocol in Event-B. DSR is a reactive routing protocol, which finds a route for a destination on demand, whenever communication is needed. Route discovery is an important task of any routing algorithm and formal specification of it, itself is a challenging problem. The specification is performed in a stepwise manner composing more advanced routing components between the abstract specification and topology. It is verified through a series of refinements. The specification includes safety properties as set of invariants, and liveness properties that characterize when the system reaches stable states. We establish these properties by proof of invariants, event refinement and deadlock freedom. The consequence of this incremental approach helps to achieve a high degree of automatic proof. Our approach can be useful for formalizing and developing other kinds of reactive routing protocols (i.e. AODV etc.).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Johnson, D.B., Maltz, D.A.: Dynamic Source Routing in Ad Hoc Wireless Networks. In: Mobile Computing. The International Series in Engineering and Computer Science, vol. 353, pp. 153–181. Springer, US (1996) ISSN 0893-3405
Project RODIN: Rigorous open development environment for complex systems (2004), http://rodin-b-sharp.sourceforge.net/ (2004-2007)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Hoang, T.S., Kuruma, H., Basin, D.A., Abrial, J.R.: Developing Topology Discovery in Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 1–19. Springer, Heidelberg (2009)
Cansell, D., Méry, D.: The Event-B Modelling Method: Concepts and Case Studies, pp. 33–140. Springer, Heidelberg (2007); See [12]
Leavens, G.T., Abrial, J.R., Batory, D.S., Butler, M.J., Coglio, A., Fisler, K., Hehner, E.C.R., Jones, C.B., Miller, D., Jones, S.L.P., Sitaraman, M., Smith, D.R., Stump, A.: Roadmap for enhanced languages and methods to aid verification. In: Proceedings of the 5th Inter. Conf. on Generative Programming and Component Engineering (GPCE), pp. 221–236 (2006)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Wibling, O., Parrow, J., Pears, A.: Automatized Verification of Ad Hoc Routing Protocols, pp. 343–358. Springer, Heidelberg (2004)
Abrial, J.R., Cansell, D., Méry, D.: A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol. Formal Asp. Comput. 14(3), 215–227 (2003)
Yang, H., Zhang, X., Wang, Y.: A Correctness Proof of the DSR Protocol. In: Cao, J., Stojmenovic, I., Jia, X., Das, S.K. (eds.) MSN 2006. LNCS, vol. 4325, pp. 72–83. Springer, Heidelberg (2006)
Cavalli, A., Grepet, C., Maag, S., Tortajada, V.: A Validation Model for the DSR Protocol. In: Proceedings of the 24th ICDCSW 2004, vol. 7, pp. 768–773. IEEE Computer Society, Los Alamitos (2004)
Bjørner, D., Henson, M.C. (eds.): Logics of Specification Languages. EATCS Textbook in Computer Science. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Méry, D., Singh, N.K. (2011). Analysis of DSR Protocol in Event-B. In: Défago, X., Petit, F., Villain, V. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2011. Lecture Notes in Computer Science, vol 6976. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24550-3_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-24550-3_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24549-7
Online ISBN: 978-3-642-24550-3
eBook Packages: Computer ScienceComputer Science (R0)