In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs i...In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs in interdomain systems has quite recently become a significant focus of research. A framework for checking SPPs is presented in this paper with verification of an interdomain routing system using formal methods and the NuSMV software. Sufficient conditions and necessary conditions for determining SPP occurrence are presented with proof of the method＇s effectiveness. Linear temporal logic was used to model an interdomain routing system and its properties were analyzed. An example is included to demon- strate the method＇s reliability.展开更多
This paper presents a novel approach for checking route oscillation of border gateway protocol（BGP） quickly,by which the privacy of routing policies of autonomous system（AS） can be respected.Firstly,route update c...This paper presents a novel approach for checking route oscillation of border gateway protocol（BGP） quickly,by which the privacy of routing policies of autonomous system（AS） can be respected.Firstly,route update chain tag（RUCT） is constructed to track the forwarding of update report,and local routing library is made to record the changing history of update report.Then route oscillation can be identified by analyzing correlative state of RUCT and local routing library.The characteristic of this approach is that an arbitrary AS can check route oscillation alone only by sharing its network ID,which greatly respects the pri-vacy of routing policies for each AS.This paper shows that both looping in RUCT and consecutive positive-negative report in local record are sufficient conditions for route oscillation.Comparative experiments demonstrate the availability and efficiency of the proposed approach.展开更多
基金Supported by the Basic Research Foundation of Tsinghua National Laboratory for Information and Technology (TNList)the JSPS Foundation
文摘In networks, the stable path problem （SPP） usually results in oscillations in interdomain systems and may cause systems to become unstable. With the rapid development of internet technology, the occurrence of SPPs in interdomain systems has quite recently become a significant focus of research. A framework for checking SPPs is presented in this paper with verification of an interdomain routing system using formal methods and the NuSMV software. Sufficient conditions and necessary conditions for determining SPP occurrence are presented with proof of the method＇s effectiveness. Linear temporal logic was used to model an interdomain routing system and its properties were analyzed. An example is included to demon- strate the method＇s reliability.
基金National Basic Research Program of China (2011CB707000)Foundation for Innovative Research Groups of the National Natural Science Foundation of China (60921001)
文摘This paper presents a novel approach for checking route oscillation of border gateway protocol（BGP） quickly,by which the privacy of routing policies of autonomous system（AS） can be respected.Firstly,route update chain tag（RUCT） is constructed to track the forwarding of update report,and local routing library is made to record the changing history of update report.Then route oscillation can be identified by analyzing correlative state of RUCT and local routing library.The characteristic of this approach is that an arbitrary AS can check route oscillation alone only by sharing its network ID,which greatly respects the pri-vacy of routing policies for each AS.This paper shows that both looping in RUCT and consecutive positive-negative report in local record are sufficient conditions for route oscillation.Comparative experiments demonstrate the availability and efficiency of the proposed approach.
