The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - April (2010 vol.59)
pp: 561-573
Hao Zheng , University of South Florida, Tampa
Haiqiong Yao , University of South Florida, Tampa
Tomohiro Yoneda , National Institute of Informatics, Japan
ABSTRACT
Divide-and-conquer is essential to address state explosion in model checking. Verifying each individual component in a system, in isolation, efficiently requires an appropriate context, which traditionally is obtained by hand. This paper presents an efficient modular model checking approach for asynchronous design verification. It is equipped with a novel abstraction refinement method that can refine a component abstraction to be accurate enough for successful verification. It is fully automated, and eliminates the need of finding an accurate context when verifying each individual component, although such a context is still highly desirable. This method is also enhanced with additional state space reduction techniques. The experiments on several nontrivial asynchronous designs show that this method efficiently removes impossible behaviors from each component including ones violating correctness requirements.
INDEX TERMS
Formal methods, model checking, modular verification, logic verification, circuit verification, abstraction, refinement.
CITATION
Hao Zheng, Haiqiong Yao, Tomohiro Yoneda, "Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement", IEEE Transactions on Computers, vol.59, no. 4, pp. 561-573, April 2010, doi:10.1109/TC.2009.187
REFERENCES
[1] R. Alur, L. de Alfaro, T. Henzinger, and F. Mang, "Automating Modular Verification," Proc. 10th Int'l Conf. Concurrency Theory, pp. 82-97, 1999.
[2] R. Alur, P. Madhusudan, and W. Nam, "Symbolic Compositional Verification by Learning Assumptions," Proc. Int'l Conf. Computer Aided Verification, pp. 548-562, 2005.
[3] S. Berezin, S. Campos, and E. Clarke, "Compositional Reasoning in Model Checking," Proc. COMPOS, pp. 81-102, Sept. 1998.
[4] M. Bobaru, C. Pasareanu, and D. Giannakopoulou, "Automated Assume-Guarantee Reasoning by Abstraction Refinement," Proc. Int'l Conf. Computer Aided Verification, 2008.
[5] D. Bustan and O. Grumberg, "Modular Minimization of Deterministic Finite-State Machines," Proc. Sixth Int'l Workshop Formal Methods for Industrial Critical Systems (FMICS '01), July 2001.
[6] S. Chaki, E. Clarke, J. Ouaknine, and N. Sharygina, "Automated, Compositional and Iterative Deadlock Detection," Proc. Int'l Conf. Formal Methods and Models for Co-Design (MEMOCODE '04), pp. 201-210, 2004.
[7] S. Chaki, E. Clarke, N. Sinha, and P. Thati, "Automated Assume-Guarantee Reasoning for Simulation Conformance," Proc. Int'l Conf. Computer Aided Verification, pp. 534-547, 2005.
[8] S. Cheung and J. Kramer, "Context Constraints for Compositional Reachability Analysis," ACM Trans. Software Eng. and Methodology, vol. 5, no. 4, pp. 334-377, 1996.
[9] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "Counterexample-Guided Abstraction Refinement for Symbolic Model Checking," J. ACM, vol. 50, no. 5, pp. 752-794, 2003.
[10] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 2001.
[11] E. Clarke, A. Gupta, J. Kukula, and O. Shrichman, "Sat Based Abstraction-Refinement Using ILP and Machine Learning Techniques," Proc. Int'l Workshop Computer Aided Verification, pp. 265-279, 2002.
[12] E. Clarke, D. Long, and K. McMillan, "Compositional Model Checking," Proc. Fourth Ann. Symp. Logic in Computer Science, pp. 353-362, 1989.
[13] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "Counterexample-Guided Abstraction Refinement," Proc. Intl. Conf. Computer Aided Verification, pp. 154-169, 2000.
[14] J. Cobleigh, G. Avrunin, and L. Clarke, "Breaking Up Is Hard to Do: An Investigation of Decomposition for Assume-Guarantee Reasoning," Proc. 2006 Int'l Symp. Software Testing and Analysis, pp. 97-108, 2006.
[15] J. Cobleigh, D. Giannakopoulou, and C. Pasareanu, "Learning Assumptions for Compositional Verification," Proc. Int'l Conf. Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 331-346, 2003.
[16] L. de Alfaro and T. Henzinger, "Interface Automata," Proc. Eighth European Software Eng. Conf. Held Jointly with Ninth ACM SIGSOFT Int'l Symp. Foundations of Software Eng. (ESEC/FSE-9), pp. 109-120, 2001.
[17] L. de Alfaro and T. Henzinger, "Interface Theories for Component-Based Design" Proc. First Int'l Workshop Embedded Software, pp. 148-165, Oct. 2001.
[18] L. de Alfaro and T. Henzinger, "Interface-Based Design," Engineering Theories of Software-Intensive Systems, vol. 195, pp. 83-104, Springer, 2005.
[19] D. Dill, "Trace Theory for Automatic Hierarchical Verification of Speed Independent Circuits," PhD thesis, Carnegie Mellon Univ., 1988.
[20] M. Gheorghiu, D. Giannakopoulou, and C.S. Pasareanu, "Refining Interface Alphabets for Compositional Verification," Proc. Int'l Conf. Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2007.
[21] D. Giannakopoulou, C.S. Pasareanu, and H. Barringer, "Component Verification with Automatically Generated Assumptions," Automated Software Engineering, pp. 297-320, Kluwer Academic Publishers, 2005.
[22] S. Graf, B. Steffen, and G. Luttgen, "Compositional Minimization of Finite State Systems Using Interface Specifications," Formal Aspects of Computation, vol. 8, no. 5, pp. 607-616, 1996.
[23] O. Grumberg and D. Long, "Model Checking and Modular Verification," ACM Trans. Programming Languages and Systems, vol. 16, no. 3, pp. 843-871, May 1994.
[24] T. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer, "Thread-Modular Abstraction Refinement," Proc. Int'l Conf. Computer Aided Verification, pp. 262-274, 2003.
[25] T. Henzinger, S. Qadeer, and S. Rajamani, "You Assume, We Guarantee: Methodology and Case Studies," Proc. Int'l Conf. Computer Aided Verification, pp. 440-451, 1998.
[26] G.J. Holzmann, "The Model Checker SPIN," IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, May 1997.
[27] J. Krimm and L. Mounier, "Compositional State Space Generation from Lotos Programs," Proc. Int'l Conf. Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 239-258, 1997.
[28] F. Lang, "Refined Interface for Compositional Verification," Proc. Int'l Conf. Formal Techniques for Networked and Distributed Systems (FORTE '06), 2006.
[29] A.J. Martin, "Self-Timed FIFO: An Exercise in Compiling Programs into VLSI Circuits," Technical Report 1986.5211-tr-86, California Inst. of Tech nology, 1986.
[30] K.L. Mcmillan, "A Methodology for Hardware Verification Using Compositional Model Checking," technical report, Cadence Berkeley Labs, 1999.
[31] C.J. Myers, Asynchronous Circuit Design. Wiley Inter-Science, 2001.
[32] C.J. Myers, W. Belluomini, K. Killpack, E. Mercer, E. Peskin, and H. Zheng, "Timed Circuits: A New Paradigm for High-Speed Design," Proc. Asia and South Pacific Design Automation Conf., pp. 335-340, 2001.
[33] W. Nam and R. Alur, "Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition," Proc. Int'l Symp. Automated Technology for Verification and Analysis (ATVA), 2006.
[34] A. Pnueli, "In Transition from Global to Modular Temporal Reasoning about Programs," Logics and Models of Concurrent Systems, pp. 123-144, Springer-Verlag, 1989.
[35] K. Stevens, R. Ginosar, and S. Rotem, "Relative Timing," Proc. Int'l Symp. Advanced Research in Asynchronous Circuits and Systems, pp. 208-218, 1999.
[36] H. Yao and H. Zheng, "Automated Interface Refinement for Compositional Verification," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 28, no. 3, pp. 433-446, Mar. 2009.
[37] T. Yoneda and T. Yoshikawa, "Using Partial Orders for Trace Theoretic Verification of Asynchronous Circuits," Proc. Int'l Symp. Advanced Research in Asynchronous Circuits and Systems, Mar. 1996.
[38] H. Zheng, C. Myers, D. Walter, S. Little, and T. Yoneda, "Verification of Timed Circuits with Failure Directed Abstractions," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 25, no. 3, pp. 403-412, Mar. 2006.
26 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool