时间自动机与网络协议验证

doi:10.3969/j.issn.1000-3428.2006.22.047

计算机工程 ›› 2006, Vol. 32 ›› Issue (22): 130-132. doi: 10.3969/j.issn.1000-3428.2006.22.047

时间自动机与网络协议验证

高冠龙1，周清雷1,2

(1. 郑州大学信息工程学院，郑州 450052；2. 信息工程大学信息工程学院，郑州 450002)

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2006-10-20 发布日期:2006-10-20

Timed Automata and Network Protocol Verification

GAO Guanlong1, ZHOU Qinglei1,2

(1. School of Information Engineering, Zhengzhou University, Zhengzhou 450052 ; 2. School of Information Engineering, Information Engineering University, Zhengzhou 450002)

Received:1900-01-01 Revised:1900-01-01 Online:2006-10-20 Published:2006-10-20

摘要/Abstract

摘要： 随着网络协议复杂性的增大，其自身的潜在错误变得更加重要。使用形式化的方法来描述和验证网络协议可以发现其中的潜在错误。时间自动机是形式化方法的一种，可以很好地应用于网络协议验证中。目前基于时间自动机已经开发出了多种自动验证工具。文章介绍了网络协议验证的几种方法，并以KRONOS验证FDDI协议为例说明了用时间自动机验证协议的方法。

关键词: 时间自动机, 网络协议, 协议验证

Abstract: The protocol complexity is increasing rapidly, it is important to discover the faulty in protocols. There are many verification methods for protocols. Timed automata can also be applied in protocol verifications very well. Many tools have been developed based on timed automata. They are very useful in protocol verifications. This paper presents some methods of protocol verification and uses KRONOS to verify FDDI to introduce the method of using timed automata.

Key words: Timed automata, Network protocol, Protocol verification

中图分类号:

TP301.1

高冠龙;周清雷;. 时间自动机与网络协议验证[J]. 计算机工程, 2006, 32(22): 130-132.

GAO Guanlong; ZHOU Qinglei;. Timed Automata and Network Protocol Verification[J]. Computer Engineering, 2006, 32(22): 130-132.

http://www.ecice06.com/CN/Y2006/V32/I22/130

[1]	黄小兵, 聂兰顺. OPEN-MAC:一种低功耗有保障下行的网络架构[J]. 计算机工程, 2019, 45(10): 101-109.
[2]	唐郑熠,王金水,何栋炜,薛醒思,胡文瑜. 馈线自动化算法的形式化建模与验证[J]. 计算机工程, 2016, 42(3): 89-93.
[3]	潘道欣,王轶骏,薛质. 基于网络协议逆向分析的远程控制木马漏洞挖掘[J]. 计算机工程, 2016, 42(2): 146-150,156.
[4]	杨晓波. Web服务编制的形式化模型研究[J]. 计算机工程, 2012, 38(7): 276-278.
[5]	于淼, 李允, 桂盛霖, 罗蕾. 基于时间自动机的嵌入式系统调度分析工具[J]. 计算机工程, 2012, 38(3): 290-292.
[6]	王彦哲, 汪歆, 邱依昕, 潘强. 传感器网络信息处理支撑服务测试研究[J]. 计算机工程, 2012, 38(2): 119-122.
[7]	智少磊, 夏继强, 张炯. 基于OPC的服务机器人监控系统设计[J]. 计算机工程, 2012, 38(14): 266-268.
[8]	张磊 , 马光胜, 修建新. 任务网络到时间自动机的等价模型验证[J]. 计算机工程, 2012, 38(13): 286-288.
[9]	李向燕, 唐柳湘, 李允. 基于AUTOSAR的LIN实现[J]. 计算机工程, 2012, 38(04): 208-211.
[10]	王文化, 沈庆国, 韩春永, 王滨, 戴三明. 基于染色Petri网的BGP连接过程模型[J]. 计算机工程, 2011, 37(6): 82-84.
[11]	廖伟志, 李文敬, 王汝凉. ICPN的时间自动机构造方法[J]. 计算机工程, 2011, 37(6): 15-17.
[12]	房小兆, 张巍, 滕少华, 韩娜. 基于δ-HSSVM的协同入侵检测方法[J]. 计算机工程, 2011, 37(21): 100-101,104.
[13]	张翼, 周四望. 基于历史相遇间隔的机会网络路由协议[J]. 计算机工程, 2011, 37(14): 85-87.
[14]	顾翔;邱建林;邵浩然. 基于RSL的协议形式化描述与验证方法[J]. 计算机工程, 2009, 35(23): 41-43.
[15]	范昊;吴哲辉. 基于CPEBSDL通信协议的Petri网建模方法[J]. 计算机工程, 2008, 34(6): 16-21.

选择文件类型/文献管理软件名称

选择包含的内容

时间自动机与网络协议验证

Timed Automata and Network Protocol Verification

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

时间自动机与网络协议验证

Timed Automata and Network Protocol Verification

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价