并发程序的切片模型检验方法  

Slicing Concurrent Programs for Model Checking

作　　者：董威[1] 王戟[1] 齐治昌[1] 

机构地区：[1]国防科学技术大学计算机学院,长沙410073

出　　处：《计算机学报》2003年第3期266-274,共9页Chinese Journal of Computers

基　　金：国家"八六三"高技术研究发展计划 ( 2 0 0 1AA113 2 0 2 );国家自然科学基金( 69973 0 5 1;90 10 40 0 7);霍英东青年教师基金 ( 710 64 )资助

摘　　要：提出了一种对并发程序进行切片以缩减模型检验状态空间的方法 .首先针对并发程序中的同步与通信定义了一组依赖关系 ,包括并发分支与接合、非确定性、信道、共享变量等特征 .对于从要验证的时态逻辑性质中提取的关于多个程序点的切片标准 ,文中给出算法根据相应的依赖关系通过不动点运算得到并发程序切片 .Model checking is an important technology of automatic verification, and its main problem faced is space-explosion, which is usually caused by the concurrency in the system. This paper presents an efficient approach to slice concurrent programs for model checking. A set of dependence relations is defined corresponding to the characteristics of synchronization and communication in concurrent programs, such as parallel fork and joint, non-deterministic, channel, share variable, and lock. The dependence graph of concurrent program can be constructed from these dependence relations. To ensure the correctness of verification result for temporal property, the multi-points-relevant slicing criterion is extracted from the property. Then, the paper presents a method to compute the slice of concurrent program, which only includes the statements reachable from the slicing criterion in dependence graph. The correctness of the resulted slice is guaranteed with respect to the satisfaction of the desired property. The method throws away the irrelevant portions of the program corresponding to the property, which will reduce the state space to be explored in model checking. Finally, slicing is compared with partial-order reduction, another method that reduces the state space according to the property, and the similarities and differences of these two methods are discussed.

关 键 词：并发程序 模型检验 程序切片 自动验证 JAVA语言 SPL语言 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]