%0 Journal Article
%T Formal Verification of IPv6 Neighbor Discovery Protocol<br>IPv6邻居发现协议的形式化验证
%A YE Xin-Ming
%A HAO Song-Xia
%A <br>叶新铭
%A 郝松侠
%J 软件学报
%D 2005
%I 
%X 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.
%K message sequence charts
%K model checking
%K formal verification
%K automata theory<br>消息序列表
%K 模型检查
%K 形式化验证
%K 自动机理论
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=ABEF4247901D2012&yid=2DD7160C83D0ACED&vid=7801E6FC5AE9020C&iid=B31275AF3241DB2D&sid=7CCBDF94263DBB99&eid=53A4507B400B4E65&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=10