Dynamic Routing Protocols Evaluation With The Feedback of Event-B and Formal Method
the goal of this Paper is to explore message passing in dynamic routing with the use of formal methods.
Nowadays, one of the core research directions in a constantly growing distributed environment is the improvement of the
communication process. The responsibility for proper verification becomes crucial. Formal methods can play an essential
role in the development and testing of systems. The paper presents different methodologies for assessing correctness. Our
approach employs abstract interpretation techniques for creating trace based model for protocols in dynamic routing and
message passing. The models used for building a semi decidable procedure for verifying the system model. We also defines
the networks addresses in network layer of OSI model which routers are operating in this layer. Network layer routes data
from one node to another and determine best path to destination. Also the network layer of the OSI model, provides an endto-
end logical addressing system so that a packet of data can be routed across several layer 2 networks (Ethernet, Token
Ring, Frame Relay, etc.). Note that network layer addresses can also be referred to as logical addresses. Initially, software
manufacturers, such as Novell, developed proprietary layer 3 addressing. However, the networking industry has evolved to
the point that it requires a common layer 3 addressing system. The Internet Protocol (IP) addresses make networks easier to
both set up and connect with one another. The Internet uses IP addressing to provide connectivity to millions of networks
around the world.
Keywords- Dynamic Routing, Formal Method, Event-B