| IPv6邻居发现协议的形式化验证 |
| |
| 引用本文： | 叶新铭,郝松侠.IPv6邻居发现协议的形式化验证[J].软件学报,2005,16(6):1182-1189. |
| |
| 作者姓名： | 叶新铭 郝松侠 |
| |
| 作者单位： | 1. 内蒙古大学,计算机学院,内蒙古,呼和浩特,010021
2. 中国科学院,软件中心,北京,100080 |
| |
| 基金项目： | Supported by the National Natural Science Foundation of China under Grant No.60263002 (国家自然科学基金); the Key Science-Technology Project of Inner Mongolia under Grant No.2002061002 (内蒙古科技攻关项目) |
| |
| 摘 要： | 采用模型检查技术,对IPv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的MSC(message sequence charts)来描述,并通过线性时序逻辑说明该协议的属性.还提出了由MSC模型的线性化自动抽取协议属性的方法.
|
| 关 键 词： | 消息序列表 模型检查 形式化验证 自动机理论 |
| 文章编号： | 1000-9825/2005/16(06)1182 |
| 收稿时间： | 2003/9/28 0:00:00 |
| 修稿时间： | 5/8/2004 12:00:00 AM |
Formal Verification of IPv6 Neighbor Discovery Protocol |
| |
| YE Xin-Ming and HAO Song-Xia.Formal Verification of IPv6 Neighbor Discovery Protocol[J].Journal of Software,2005,16(6):1182-1189. |
| |
| Authors: | YE Xin-Ming and HAO Song-Xia |
| |
| Abstract: | 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. |
| |
| Keywords: | message sequence charts model checking formal verification automata theory |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
