摘要
边界网关协议(BGP)缺少形式化分析,为此,根据RFC 1771,针对2个BGP路由器间连接建立过程,使用染色Petri网建立层级模型。通过交互式仿真观察所建模型行为和预期行为是否发生偏离。判定行为偏离发生的原因,修改模型直到偏离消失。求解模型的状态空间,并验证BGP连接过程的无死锁性和公平性。
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.
出处
《计算机工程》
CAS
CSCD
北大核心
2011年第6期82-84,共3页
Computer Engineering
关键词
边界网关协议
形式化模型
染色Petri网
协议验证
Border Gateway Protocol（BGP）
formal model
Colored Petri Net（CPN）
protocol verification
