Thumbnail
Access Restriction
Open

Author Wu, Peng ♦ Zhang, Dongmei
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Mobile Network Protocol ♦ Compositional Analysis ♦ Deadlock Freedom ♦ System Model ♦ Task Component ♦ Main Advantage ♦ Binding Coherency ♦ Unstable Route ♦ Mobile Ipv6 ♦ Model Checker ♦ Dynamic Network Topology ♦ Case Study ♦ Direct Model Checking ♦ Compositional Framework ♦ Additional Mobility Facility ♦ Modelling Framework ♦ Mobile Ipv4 ♦ Network Protocol ♦ Symbolic Transition Graph ♦ Complicated System Model
Abstract A compositional framework is proposed for modelling network protocols with symbolic transition graphs. The main advantages of the framework are that it can address dynamic network topologies without requiring additional mobility facilities; and it can work out system models that preserve deadlock freedom, namely the deadlock freedom of a system model depends only on the deadlock freedom of its each task component. Case studies with Mobile IPv4 and IPv6 illustrate the e#ectiveness of the modelling framework. The model checking experiments show that the framework can extend the capability of the model checker to deal with more complicated system models than can be dealt with by direct model checking. Moreover, some infrangibilities of Mobile IPv6 are disclosed in the sense that it can not maintain the binding coherency all the time, which may result in unreachable or unstable routes.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Publisher Date 2005-01-01