An Approach to Modeling and Verifying Router-Based Network

Network, such as Internet and Intranet, has penetrated into people´s daily life. Router is one of the essential equipments which take an important role in the network and form a large and complicated network. However, huge amounts of routers in the network make the network communication and data routing more complex. How to insure the reach ability and correct communication of Internet is a challenge. In this paper, an approach is proposed to formally model and verify the router-based network. Then, we employ a transition system (denotes TS) to model the router-based network, and make use of the Bisimulation-Quotient Algorithms to obtain the bisimulation quotient of the finite transition system, denoted TS/~. It could be easy to verify properties on the system TS/~. Any verification result for TS/~ carries over to TS and this applies to any formula expressed in either LTL, CTL, or CTL*. This approach can facilitate verification since verification problems are particularly space-critical. Finally, some important properties of routing such as routing reach ability, routing path length, are verified.