Abstract
This paper presents optimizations for verifying systems with complex time-invariant constraints. These constraints arise naturally from modeling physical systems, e.g., in establishing the relationship between different components in a system. To verify constraint-rich systems, we propose two new optimizations. The first optimization is a simple, yet powerful, extension of the conjunctivepartitioning algorithm. The second is a collection of BDD-based macro-extraction and macro-expansion algorithms to remove state variables.We showthat these two optimizations are essential in verifying constraint-rich problems; in particular, this work has enabled the verification of fault diagnosis models of the Nomad robot (an Antarctic meteorite explorer) and of the NASA Deep Space One spacecraft.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bapna, D., Rollins, E., Murphy, J., and Maimone, M. The Atacama Desert trek-outcomes. In Proc. of the 1998 International Conference on Robotics and Automation (May 1998), pp. 597–604.
Bernard, D. E., Dorais, G. A., Fry, C., JR., E. B. G., Kanefsky, B., Kurien, J., Millar, W., Muscettola, N., Nayak, P. P., Pell, B., Rajan, K., Rouquett, N., Smith, B., and Williams, B. Design of the remote agent experiment for spacecraft autonomy. In Proc. of the 1998 IEEE Aerospace Conference (March 1998), pp. 259–281.
Berthet, C., Coudert, O., and Madre, J. C. New ideas on symbolic manipulations of finite state machines. In 1990 IEEE Proc. of the International Conference on Computer Design (September 1990), pp. 224–227.
Bryant, R. E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35, 8 (August 1986), 677–691.
Burch, J. R., Clarke, E. M., Long, D. E., Mc Millan, K. L., and Dill, D. L. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 13, 4 (April 1994), 401–424.
Coudert, O., and Madre, J. C. Aunified framework for the formal verification of circuits. In Proc. of the International Conference on Computer-Aided Design (Feb 1990), pp. 126–129.
Geist, D., and Beer, I. Efficient model checking by automated ordering of transition relation partitions. In Proc. of the Computer Aided Verification (June 1994), pp. 299–310.
Hu, A. J., and Dill, D. L. Reducing BDD size by exploiting functional dependencies. In Proc. of the 30th ACM/IEEE Design Automation Conference (June 1993), pp. 266–71.
Lin, B., and Newton, A. R. Exact redundant state registers removal based on binary decision diagrams. IFIP Transactions A, Computer Science and Technology A, 1 (August 1991), 277–86.
McMillan, K. L. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
Ranjan, R. K., Aziz, A., Brayton, R. K., Plessier, B., and Pixley, C. Efficient BDD algorithms for FSM synthesis and verification. Presented in the IEEE/ACM International Workshop on Logic Synthesis, May 1995.
Sentovich, E. M., and Horia Toma, G. B. Latch optimization in circuits generated from high-level descriptions. In Proc. of the International Conference on Computer-Aided Design (November 1996), pp. 428–35.
Shiple, T. R., Hojati, R., Sangiovanni-Vincentelli, A. L., and Brayton, R. K. Heuristic minimization of BDDs using don’t cares. In Proc. of the 31st ACM/IEEE Design Automation Conference (June 1994), pp. 225–231.
Van Eijk, C. A. J., and Jess, J. A. G. Exploiting functional dependencies in finite state machine verification. In Proc. of European Design and Test Conference (March 1996), pp. 266–71.
Williams, B. C., and Nayak, P. P. A model-based approach to reactive self-configuring systems. In Proc. of the Thirteenth National Conference on Artificial Intelligence and the Eighth Innovative Applications of Artificial Intelligence Conference (August 1996), pp. 971–978.
Yang, B., Bryant, R. E., O’Hallaron, D. R., Biere, A., Coudert, O., Janssen, G., Ranjan, R. K., and Somenzi, F. A performance study of BDD-based model checking. In Proc. of the Formal Methods on Computer-Aided Design (November 1998), pp. 255–289.
Yang, B., Simmons, R., Bryant, R. E., and O’Hallaron, D. R. Optimizing symbolic model checking for constraint-rich models. Tech. Rep. CMU-CS-99-118, School of Computer Science, Carnegie Mellon University, March 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, B., Simmons, R., Bryant, R.E., O’Hallaron, D.R. (1999). Optimizing Symbolic Model Checking for Constraint-Rich Models. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_29
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive