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

Slicing Concurrent Programs for Model Checking

提出了一种对并发程序进行切片以缩减模型检验状态空间的方法 .首先针对并发程序中的同步与通信定义了一组依赖关系 ,包括并发分支与接合、非确定性、信道、共享变量等特征 .对于从要验证的时态逻辑性质中提取的关于多个程序点的切片标准 ,文中给出算法根据相应的依赖关系通过不动点运算得到并发程序切片 .

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.