| 摘要: |
| 采用模型检查技术,对IPv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的MSC(message sequence charts)来描述,并通过线性时序逻辑说明该协议的属性.还提出了由MSC模型的线性化自动抽取协议属性的方法. |
| 关键词: 消息序列表 模型检查 形式化验证 自动机理论 |
| DOI： |
| 分类号: |
| 基金项目: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 (内蒙古科技攻关项目) |
|
| Formal Verification of IPv6 Neighbor Discovery Protocol |
|
YE Xin-Ming,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. |
| Key words: message sequence charts model checking formal verification automata theory |
