The 3rd ACS/IEEE International Conference onComputer Systems and Applications, 2005.
Download PDF

Abstract

Summary form only given. As the model-checking (which is based on reachability analysis) becomes increasingly used in the industry, there is a big need for efficient new methods to deal with the large real-size designs. This paper presents a novel method for improving the performance of reachability analysis using parallelization techniques. We propose a new method for partitioning the large state space modeling industrial designs with hundreds of millions of states and transitions. This method partitions the state space by performing a combination of abstraction-partition-refinement on its structure. The reachability analysis is distributed on processes located on the different network machines. Each one owns a partition and executes the reachability analysis on it. The algorithm for parallel reachability analysis is designed by a way reducing the communication overhead between the processes. The experimental results on large real designs show that this method improves the quality of partitions, the communication overhead and then the overall performance of the reachability analysis.
Like what you’re reading?
Already a member?Sign In
Member Price
$11
Non-Member Price
$21
Add to CartSign In
Get this article FREE with a new membership!