微信服务号

微信订阅号

2025年4月15日 23:17 星期二
首页 > 过刊浏览>2005年第16卷第6期 >1182-1189
PDF HTML阅读 XML下载 导出引用 引用提醒
IPv6邻居发现协议的形式化验证
作者:
基金项目:

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
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [10]
    • |
  • 相似文献 [20]
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    采用模型检查技术,对IPv6的邻居发现协议的属性进行了形式化验证.该协议的模型由目前广泛用于设计和描述通信协议的MSC(message sequence charts)来描述,并通过线性时序逻辑说明该协议的属性.还提出了由MSC模型的线性化自动抽取协议属性的方法.

    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.

    参考文献
    [1]ITU-T.ITU-T Recommendation Z.120, Message Sequence Chart (MSC), 1999.
    [2]Pratt V. Modeling concurrency with partial orders. Int'l Journal of Parallel Programming, 1986,15(1):33-71.
    [3]Peled D. Specification and verification of message sequence charts. In: Bolognesi T, Latella D, eds. Proc. of the Formal Methods for Distributed System Development. Pisa: Kluwer Academic Publishers, 2000. 139-154.
    [4]Alur R, Peled D, Penczek W. Model-Checking of causality properties. In: Proc. of the Proc. of the 10th Annual IEEE Symp. on Logic in Computer Science. San Diego: IEEE Computer Society Press, 1995.90-100.
    [5]Muscholl A, Peled D, Su Z. Deciding properties for message sequence charts. In: Nivat M, ed. Proc. of the FoSSaCS 1998, LNCS 1378. Berlin: Springer-Verlag, 1998.226-242.
    [6]Alur R, Yannakakis M. Model checking of message sequence charts. In: Baeten JCM, Mauw S, eds. Proc. of the CONCUR'99,Concurrency Theory. LNCS 1664, Berlin: Springer-Verlag, 1999. 114-129.
    [7]Narten T, Nordmark E, Simpson W. Neighbor discovery for IP version 6 (IPv6). RFC 2461, 1998.
    [8]Kindler E. Safety and liveness properties: A survey. EATCS-BuUetin, 1994,53:268-272.
    [9]Deussen PH, Tobies S. Formal test purposes and the validity of test cases. In: Peled DA, Vardi MY, eds. Proc. of the FORTE 2002.LNCS 2529, Berlin: Springer-Verlag, 2002.114-129.
    [10]Holzmann HJ. The model checker spin. IEEE Trans. on Software Engineering, 1997,23(5):279-295.
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

叶新铭,郝松侠. IPv6邻居发现协议的形式化验证.软件学报,2005,16(6):1182-1189

复制
分享
文章指标
  • 点击次数:3703
  • 下载次数: 5883
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2003-09-28
  • 最后修改日期:2004-05-08
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19828277位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号