论文部分内容阅读
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 frame-work 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.
With 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 frame-work 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 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.