Analysis of DSR Protocol in Event-B

Dominique Méry 1 Neeraj Kumar Singh 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.).
Type de document :
Communication dans un congrès
Défago, Xavier and Petit, Franck and Villain, Vincent. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. Springer Berlin / Heidelberg, 6976, pp.401-415, 2011, Stabilization, Safety, and Security of Distributed Systems. 〈http://dx.doi.org/10.1007/978-3-642-24550-3_30〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00637768
Contributeur : Neeraj Kumar Singh <>
Soumis le : mercredi 2 novembre 2011 - 18:45:43
Dernière modification le : mardi 24 avril 2018 - 13:37:37

Identifiants

  • HAL Id : inria-00637768, version 1

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. Analysis of DSR Protocol in Event-B. Défago, Xavier and Petit, Franck and Villain, Vincent. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. Springer Berlin / Heidelberg, 6976, pp.401-415, 2011, Stabilization, Safety, and Security of Distributed Systems. 〈http://dx.doi.org/10.1007/978-3-642-24550-3_30〉. 〈inria-00637768〉

Partager

Métriques

Consultations de la notice

273