Formal Development of Path Discovery in AODV Routing Protocol using Event-B | Zendy

Arun Kumar | Zendy; Divakar Yadav | Zendy; Vinod Kumar | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Formal Development of Path Discovery in AODV Routing Protocol using Event-B

Author(s) -

Arun Kumar,

Divakar Yadav,

Vinod Kumar

Publication year - 2015

Publication title -

international journal of computer applications

Language(s) - English

Resource type - Journals

ISSN - 0975-8887

DOI - 10.5120/ijca2015905481

Subject(s) - computer science , path (computing) , event (particle physics) , protocol (science) , development (topology) , computer network , medicine , physics , mathematics , mathematical analysis , alternative medicine , pathology , quantum mechanics

In this paper, we present a formal model for path discovery process of the AODV protocol using Event-B. The model have been developed and checked using the RODIN tool which provides an integrated framework for development of Event-B models. Event-B technique uses a notion of refinement to specify the mathematical models of distributed systems in an incremental manner. The specifications of the system have been checked for consistency and satisfy the behavioural properties of the system expressed as invariants. All the proof obligations were discharged automatically by the RODIN tool.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research