摘要
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.
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.
基金
Supported by the Basic Research Foundation of Tsinghua National Laboratory for Information and Technology (TNList)
the JSPS Foundation
