基于模型检查的TCP连接管理协议分析与验证

• 作者: 周志远 张大方 缪力 黄谷
• 来源期刊: 计算机工程与设计
• 学科: 工学
• 关键词: 模型检查 形式化验证 有限状态机 线形时序逻辑 TCP连接管理
• 年，卷（期）: 2009,（10）
• 所属期刊栏目: 信息安全技术
• 页码范围: 2381-2386
• 页数: 6页
• 分类号: TP311.5
• 字数: 6795字
• 语种: 中文

摘要

随着网络协议复杂性的增大,如何发现其自身的潜在错误变得非常重要.为了发现传统测试手段难以检测的错误,采用模型检查技术分析和验证网络协议.从TCP协议设计规范中提取了包含TCP连接管理协议重要细节的形式化模型,并采用模型检查工具SPIN验证协议模型是否满足需求,结果表明,TCP协议设计规范中同同时打开连接过程存在不一致问题,针对该问题提出了改进策略.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张大方	湖南大学软件学院	295	2498	22.0	33.0
2	缪力	湖南大学软件学院	35	167	8.0	10.0
3	黄谷	湖南大学软件学院	2	2	1.0	1.0
4	周志远	湖南大学软件学院	3	16	2.0	3.0