Abstract
This work presents a novel distributed, symbolic algorithm for reachability analysis that can effectively exploit, “as needed”, a large number of machines working in parallel. The novelty of the algorithm is in its dynamic allocation and reallocation of processes to tasks and in its mechanism for recovery, from local state explosion. As a result, the algorithm is work-efficient: it utilizes only those resources that are actually needed. In addition, its high adaptability makes it suitable for exploiting the resources of very large and heterogeneous distributed, non-dedicated environments. Thus, it has the potential of verifying very large systems.
We implemented our algorithm in a tool called Division. Our preliminary experimental results show that the algorithm is indeed work-efficient. Although that the goal of this research is to check larger models, the results also indicate the potential to obtain high speedups, because communication overhead is very small.
Chapter PDF
References
Amla, N., Kurshan, R., McMillan, K., Medel, R.K.: Experimental Analysis of Different Techniques for Bounded Model Checking. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 34–48. Springer, Heidelberg (2003)
Beer, I., Ben-David, S., Eisner, C., Landver, A.: Rulebase: An Industry-Oriented Formal Verification Tool. In: 33rd Design Automation Conf., pp. 655–660 (1996)
Beer, I., Ben-David, S., Landver, A.: On-the-Fly Model Checking of RCTL Formulas. In: CAV 1994. LNCS, vol. 818 (1998)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking Without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: Halaas, A., Denyer, P.B. (eds.) Proc. of the 1991 Int. Conference on Very Large Scale Integration (August 1991)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–171 (1992)
Cabodi, G.: Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. In: Proc. of the 13th Int. Conf. on Computer Aided Verification (2001)
Cabodi, G., Camurati, P., Quer, S.: Improved Reachability Analysis of Large FSM. In: Proc. of the IEEE Int. Conf. on Computer Aided Design, pp. 354–360. IEEE Computer Society Press, Los Alamitos (1996)
Cabodi, G., Camurati, P., Quer, S.: Improving the Efficient of BDD-Bsaed Operators by Means of Partitioning. IEEE Transactions on Computer-Aided Design (May 1999)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Geist, D., Beer, I.: EfficientModel Checking by Automated Ordering of Transition Relation Partitions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 299–310. Springer, Heidelberg (1994)
Grumberg, O., Heyman, A., Heyman, T., Schuster, A.: Division System: A General Platform for Distributed Symbolic Model Checking Research (2003), http://www.cs.technion.ac.il/Labs/dsl/projects/division_web/division.htm
Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. Formal Methods in System Design 21(2), 317–338 (2002)
McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)
Milvang-Jensen, K., Hu, A.J.: BDDNOW: A parallel BDD package. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 501–507. Springer, Heidelberg (1998)
Narayan, A., Isles, A., Jain, J., Brayton, R., Sangiovanni-Vincentelli, A.L.: Reachability Analysis Using Partitioned-ROBDDs. In: Proc. of the IEEE Int. Conf. on Computer Aided Design, pp. 388–393. IEEE Computer Society Press, Los Alamitos (1997)
Narayan, A., Jain, J., Fujita, M., Sangiovanni-Vincentelli, A.L.: Partitioned-ROBDDs. In: Proc. of the IEEE Int. Conf. on Computer Aided Design, pp. 547–554. IEEE Computer Society Press, Los Alamitos (1996)
Stern, U., Dill, D.L.: Parallelizing the Murphy Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–267. Springer, Heidelberg (1997)
Stornetta, T., Brewer, F.: Implementation of an Efficient Parallel BDD Package. In: 33rd Design Automation Conf. IEEE Computer Society Press, Los Alamitos (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grumberg, O., Heyman, T., Schuster, A. (2003). A Work-Efficient Distributed Algorithm for Reachability Analysis. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive