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

摘要：

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

关键词：模型检查、形式化验证、有限状态机、线形时序逻辑、TCP连接管理

所属期刊栏目：30

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金项目60673155、90718008

在线出版日期：2009-06-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：2381-2386