期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

网络协议的一种构建性验证方法

A Compositional Approach of Network Protocol Verification
下载PDF
导出
摘要 论文提出了多层自动机映射的思想,并应用此方法构建了复杂协议的构建性验证方法,同时给出了协议构建性验证的逻辑基础和构建步骤。此法有效地避免了复杂协议验证中状态组合爆炸问题。 The paper presents an idea of multi-layer FSM mapping.Based on the idea,The authors give a compositional strategy of complex protocol verification,its logical foundation and steps of composition.This approach of verifying complex protocol can overcome the 'state explosion problem' effectively and efficiently.
作者 丛延奇 张立堃 刘英莉 刘诗笺
机构地区 哈尔滨工程大学计算机科学与技术学院
出处 《计算机工程与应用》 CSCD 北大核心 2005年第13期141-142,189,共3页 Computer Engineering and Applications
基金 黑龙江科技攻关项目资助(编号:GC03A120)
关键词 多层自动机映射 不动点 构建性验证 multi-layer FSM mapping,invariant,compositional verification
分类号 TP393 [自动化与计算机技术—计算机应用技术]
  • 相关文献

参考文献11

  • 1温涛,刘积仁,李华天.协议自动验证的可靠策略[J].软件学报,1993,4(5):38-45. 被引量：1
  • 2郭云川,古天龙,董荣胜,李凤英.Kerberos协议安全性的符号模型检验分析[J].计算机工程与应用,2003,39(29):177-180. 被引量：3
  • 3Burch J R,Clarke E M,McMillan K Let al.Symbolic model checking:1020 states and beyond[J].Information Computation,1992;98(2): 142-170.
  • 4Ralph D Jeffords,Constance L Heitmeyer.A Strategy for Efficiently Verifying Requirements Specifications Using Composition and Invariants Software Noets ACM.
  • 5G J Holzmann.The model checker SPIN[J].IEEE Transactions on Software Engineering, 1997 ; 23 (5) : 279-295.
  • 6R Jeffords,C Heitmeyer.Automatic generation of state invariants form requirements specifications[C].In:Proc Sixth ACM SIGSOFT Syrup on Foundations of Software Engineering, 1998-11.
  • 7Z Manna,A PnuelLTemporal Verification of Reactive Systems:Safety[M]. Springer-Verlag,New York ,NY, 1995.
  • 8K L McMillan.A methodology for hardware verification using compositional model checkin[J].Science of Comput Prog,2000 ;37 ;279-309.
  • 9C Heimeyer.software Cost Reduction[C].In:J J Marciniak ed.Encyclopedia of Software Engineering.second edition,John Wiley &Sons, Inc,New York ,NY,2002.
  • 10R Jeffords,C Heitmeyer.Automatic generation of state invariants form requirements specitlcations[C].In:Proc Sixth ACM SIGSOFT Syrup on Foundations of Software Engineering, 1998-11.

二级参考文献12

  • 1王育民 刘建伟.通信网的安全:理论与技术[M].西安电子科技大学出版社,1998..
  • 2B Clifford Neunman,Theodore Ts,o Kerberos.An Authentication Service for Computer Networks[J].IEEE Communications, 1994 ; 32 (9) : 33-38.
  • 3S G Stubblebine,R N Wright.An Authentication Logic with Formal Semantics Supporting Synchronization,Revocation,and Regency[J].IEEE Transactions on Software Engineering, 2002; 28 (3) : 256-285.
  • 4SMV.http ://www-cad.eecs.Berkeley.edu/-kenmcmil.
  • 5M Panti,L Spalazzi,S Tacconi.Using the NuSMV Model Checker to Verify the Kerberos Protocol[C].In:Proceeding of the 3rd Collaborative Technologies Symposium, 2002.
  • 6Stefanos Gritzalis,Diomidis Spinellis,Panagiotios Georgiadis.Security Protocols over Open Networks and Distributed Systems:Formal Methodfor Their Analysis,Design and Verification[J].Computer Communications,1999;22(8) :695-707.
  • 7M Burrows,M Abadi,R Needham.A Logic of Authentication[J].ACM Transactions on Computer Systems, 1990;8(1 ) : 18-36.
  • 8K L McMillan.Symbolic Model Checking[M].Kluwer Academic Publishers, 1993.
  • 9王育民 刘建伟.通信网的安全,理论与技术[M].西安电子科技大学出版社,1998..
  • 10Liu M T，1989年

共引文献2

计算机工程与应用
2005年 第13期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部