Slicing Concurrent Programs for Model Checking
Wei Fu Dong · Chinese Journal of Computers · 2003
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.