| 一种基于并发路径的协议验证方法 |
| |
| 引用本文： | 胡劲松,赵保华,屈玉贵.一种基于并发路径的协议验证方法[J].小型微型计算机系统,2004,25(10):1733-1736. |
| |
| 作者姓名： | 胡劲松 赵保华 屈玉贵 |
| |
| 作者单位： | 中国科学技术大学,信息技术学院,安徽,合肥,230026 |
| |
| 基金项目： | 国家自然科学基金重大研究计划项目 ( 90 10 40 10 0 )资助，自然科学基金科学部主任基金项目 ( 60 2 410 0 4)资助，教育部博士点基金项目 ( 2 0 0 0 0 3 5 80 2 )资助，安徽省自然科学基金项目 ( 0 10 42 2 0 8)资助，国家“863”计划项目 ( 2 0 0 1AA112 0 62和
2 |
| |
| 摘 要： | 通信协议验证方法中 ,可达性分析是一种方便的、易于自动化处理的、有效的协议验证方法 .但是随着通信协议的多样性和复杂性的不断增加 ,状态爆炸问题使得可达性分析变得难以实施 .本文采用分而治之的策略 ,提出一种基于并发路径的协议验证方法 .该方法将协议划分为相互独立的并发路径 ,通过逐一分析验证各并发路径 ,来实现验证整个协议的目的 .由于各并发路径的生成和分析都是相互独立的 ,整个协议验证对内存的需求仅受限于各并发路径的复杂度 ,因此有效地缓解了状态爆炸的问题
|
| 关 键 词： | 协议验证 并发路径 |
| 文章编号： | 1000-1220(2004)10-1733-04 |
Concurrent Path Based Protocol Verification |
| |
| HU Jin song,ZHAO Bao hua,QU Yu gui.Concurrent Path Based Protocol Verification[J].Mini-micro Systems,2004,25(10):1733-1736. |
| |
| Authors: | HU Jin song ZHAO Bao hua QU Yu gui |
| |
| Abstract: | Communication protocol verification is a procedure to check the logic errors of the protocol. Among the various proposed approaches, reachability analysis is the most convenient, automatic and effective one. However, the state explosion problem is principle obstacle successful verification of complex protocols. Using divide and conquer methods, our paper proposed new approach. For verifying the protocol, our approach divides the protocol into some independently concurrent paths, and verified one by one. Since the concurrent paths can be generated and verified independently, the memory requirement is limited to the individual concurrent path. Thus, the complex verification is reduced and the state explosion problem is alleviated. |
| |
| Keywords: | protocol verification concurrent path |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
