一种基于并发路径的协议验证方法  

Concurrent Path Based Protocol Verification

作　　者：胡劲松[1] 赵保华[1] 屈玉贵[1] 

机构地区：[1]中国科学技术大学信息技术学院,安徽合肥230026

出　　处：《小型微型计算机系统》2004年第10期1733-1736,共4页Journal of Chinese Computer Systems

基　　金：国家自然科学基金重大研究计划项目 ( 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

摘　　要：通信协议验证方法中 ,可达性分析是一种方便的、易于自动化处理的、有效的协议验证方法 .但是随着通信协议的多样性和复杂性的不断增加 ,状态爆炸问题使得可达性分析变得难以实施 .本文采用分而治之的策略 ,提出一种基于并发路径的协议验证方法 .该方法将协议划分为相互独立的并发路径 ,通过逐一分析验证各并发路径 ,来实现验证整个协议的目的 .由于各并发路径的生成和分析都是相互独立的 ,整个协议验证对内存的需求仅受限于各并发路径的复杂度 。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.

关 键 词：协议验证 并发路径 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]