IPv6邻居发现协议的形式化验证  

Formal Verification of IPv6 Neighbor Discovery Protocol

作　　者：叶新铭[1] 郝松侠[2] 

机构地区：[1]内蒙古大学计算机学院,内蒙古呼和浩特010021 [2]中国科学院软件中心,北京100080

出　　处：《软件学报》2005年第6期1182-1189,共8页Journal of Software

基　　金：国家自然科学基金;内蒙古科技攻关项目~~

摘　　要：采用模型检查技术,对IPv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的MSC(messagesequencecharts)来描述,并通过线性时序逻辑说明该协议的属性.还提出了由MSC模型的线性化自动抽取协议属性的方法.This paper presents the formal verification of properties of neighbor discovery protocol of IPv6 protocol suite using model checking. The protocol is modeled in MSC, whose use is popular in designing and documenting communication protocols. Linear temporal logic is adopted to specify properties of the protocol. The main result of this paper is an automatic method to extract properties from the MSC linearization directly.

关 键 词：消息序列表 模型检查 形式化验证 自动机理论 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]