摘要: 边界网关协议(BGP)缺少形式化分析,为此,根据RFC 1771,针对2个BGP路由器间连接建立过程,使用染色Petri网建立层级模型。通过交互式仿真观察所建模型行为和预期行为是否发生偏离。判定行为偏离发生的原因,修改模型直到偏离消失。求解模型的状态空间,并验证BGP连接过程的无死锁性和公平性。
关键词:
边界网关协议,
形式化模型,
染色Petri网,
协议验证
Abstract: Because the formal analysis of Border Gateway Protocol(BGP) is rare, a hierarchical model of connection process between two routers based on Colored Petri Net(CPN) is put forward according to RFC 1771. Through interactive simulation, the deviation between behavior of the proposed model and expected behavior can be observed. The proposed model should be tuned until all behavior deviations disappear. The state space of the model is calculated to validate the properties of no-deadlock and fairness.
Key words:
Border Gateway Protocol(BGP),
formal model,
Colored Petri Net(CPN),
protocol verification
中图分类号:
王文化, 沈庆国, 韩春永, 王滨, 戴三明. 基于染色Petri网的BGP连接过程模型[J]. 计算机工程, 2011, 37(6): 82-84.
WANG Wen-Hua, CHEN Qiang-Guo, HAN Chun-Yong, WANG Bin, DAI San-Meng. BGP Connection Process Model Based on Colored Petri Net[J]. Computer Engineering, 2011, 37(6): 82-84.