Abstract As the model-checking becomes increasingly used in the industry as an analysis support, there is a big need for efficient new methods to deal with the large real-size of concurrent transition systems. We propose a new algorithm for partitioning the large state space modelling industrial designs as concurrent transition systems with hundreds of millions of states and transitions. The produced partitions will be used by distributed processes for parallel system analysis. The state space is supposed to be represented by a weighted Kripke structure (this is an extension of the Kripke structure where weights are associated with the states and with the transitions). This algorithm partitions the weighted Kripke structure by performing a combination of abstraction-partition-refinement on this structure. The algorithm is designed in a way that reduces 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 system analysis.

References

[1] ANSI, “Small Computer System Interface-2,” Standard X3.131-1994, January 1994.

[2] Bell A. and Haverkort B. R., “Sequential and Distributed Model Checking of Petri Net Specifications,” Electronic Notes in Theoretical Computer Science , vol. 68, no. 4, 2002.

[3] Bourahla M. and Benmohamed M., “Predicate Abstraction and Refinement for Model Checking VHDL State Machines,” Electronic Notes in Theoretical Computer Science , vol. 66, no. 2, 2002.

[4] Brim L., Crhova J., and Yorav K., “Using Assumptions to Distribute CTL Model Checking,” Electronic Notes in Theoretical Computer Science , vol. 68, no. 4, 2002.

[5] Bui T. and Jones C., “A Heuristic for Reducing Fill in Sparse Matrix Factorization,” in Proceedings of the 6th SIAM Conference on Parallel Processing for Scientific Computing , pp. 445-452, 1993.

[6] Clarke E. M., Grumberg O., and Long D. E., “Model Checking and Abstraction,” ACM Transactions on Programming Languages and Systems , vol. 16, no. 5, pp. 1512-1542, 1994.

[7] Deo N., Graph Theory with Applications to Engineering and Computer Science , Automatic Computation, Prentice Hall, 1974.

[8] Garavel H. and Mounier L., “Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks,” Science of Computer Programming, vol. 29, no. 1, pp. 171-197, 1997.

[9] Hendrickson B. and Leland R., “A Multilevel Algorithm for Partitioning Graphs,” Technical Report SAND93-1301 , Sandia National Laboratories, 1993.

[10] Heyman T. , Geist D., Grumberg O., and Schuster A. , “Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits,” Formal Methods in System Design, vol. 21, no. 2, pp. 317-338, 2002.

[11] Karypis G. and Kumar V., “A Fast and High Quality Multilevel Scheme for Partitioning Irregular Graphs,” SIAM Journal on Scientific Computing , 1998.

[12] Kernighan B. W. and Lin S., “An Efficient Heuristic Procedure for Partitioning Graphs,” The Bell System Technical Journal , vol. 49, no. 2, pp. 291-307, 1970.

[13] Papadimitriou C. H. and Steiglitz K., Combinatorial Optimization, Prentice Hall, 1982.

[14] Romijn J., “Model Checking the HAVi Leader Election Protocol,” Technical Report SEN- R9915 , CWI, Amesterdam, The Netherlands, June 1999. Mustapha Bourahla has been a teacher-researcher since 1994 at the Computer Science Department, University of Biskra, Algeria. He was the Computer Science Department head, University of Biskra. He has been a member of the scientific committee since 1999. He holds MSc degree in computer science from the University of Montreal, Canada, 1989. He was a member of VHDL research group at Bell-Northern Research, Ottawa, Canada from Partitioning State Spaces of Concurrent Transition Systems 135 1989 until 1993. He is expected to finish his PhD in 2005.