Skip to main content
SpringerLink
Log in

A Compositional Minimization Approach for Large Asynchronous Design Verification

  • Conference paper
Model Checking Software (SPIN 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7385))

Included in the following conference series:

Abstract

This paper presents a compositional minimization approach with efficient state space reductions for verifying non-trivial asynchronous designs. These reductions can result in a reduced model that contains the exact same set of observably equivalent behavior in the original model, therefore no false counter-examples result from the verification of the reduced model. This approach allows designs that cannot be handled monolithically or with partial-order reduction to be verified without difficulty. The experimental results show significant scale-up of the compositional minimization approach using these reductions on a number of large asynchronous designs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Madhusudan, P., Nam, W.: Symbolic Compositional Verification by Learning Assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 548–562. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Berezin, S., Campos, S., Clarke, E.M.: Compositional Reasoning in Model Checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 81–102. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  3. Gheorghiu Bobaru, M., Păsăreanu, C.S., Giannakopoulou, D.: Automated Assume-Guarantee Reasoning by Abstraction Refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 135–148. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Bustan, D., Grumberg, O.: Modular minimization of deterministic finite-state machines. In: Proceedings the 6th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2001 (July 2001)

    Google Scholar 

  5. Chaki, S., Clarke, E., Sinha, N., Thati, P.: Automated Assume-Guarantee Reasoning for Simulation Conformance. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 534–547. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Cheung, S., Kramer, J.: Context constraints for compositional reachability analysis. ACM Transations on Software Engineering and Methodology 5(4), 334–377 (1996)

    Article  Google Scholar 

  7. Cheung, S., Kramer, J.: Checking safety properties using compositional reachability analysis. ACM Trans. Softw. Eng. Methodol. 8(1), 49–78 (1999)

    Article  Google Scholar 

  8. Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proceedings of the 4th Annual Symposium on Logic in Computer Science, pp. 353–362. IEEE Press, Piscataway (1989)

    Chapter  Google Scholar 

  9. Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Dill, D.: Trace Theory for Automatic Hierarchical Verification of Speed Independent Circuits. PhD thesis, Carnegie Mellon University (1988)

    Google Scholar 

  11. Giannakopoulou, D., Pǎsareǎnu, C.S., Barringer, H.: Component verification with automatically generated assumptions. Automated Software Engineering, 297–320 (2005)

    Google Scholar 

  12. Graf, S., Steffen, B., Luttgen, G.: Compositional minimization of finite state systems using interface specifications. Formal Aspects of Computation 8(5), 607–616 (1996)

    Article  MATH  Google Scholar 

  13. Grumberg, O., Long, D.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)

    Article  Google Scholar 

  14. Henzinger, T., Qadeer, S., Rajamani, S.: You Assume, we Guarantee: Methodology and Case Studies. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 440–451. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  15. Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, pp. 197–211. Chapman & Hall, Ltd., London (1995)

    Google Scholar 

  16. Krimm, J., Mounier, L.: Compositional State Space Generation from Lotos Programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 239–258. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  17. Martin, A.J.: Self-timed fifo: An exercise in compiling programs into vlsi circuits. Technical Report 1986.5211-tr-86, California Institute of Technology (1986)

    Google Scholar 

  18. Mcmillan, K.L.: A methodology for hardware verification using compositional model checking. Technical report, Cadence Berkeley Labs (1999)

    Google Scholar 

  19. Myers, C.J.: Computer-Aided Synthesis and Verification of Gate-Level Timed Circuits. PhD thesis, Stanford University (1995)

    Google Scholar 

  20. Nam, W., Alur, R.: Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 170–185. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Stevens, K., Ginosar, R., Rotem, S.: Relative timing. In: Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, pp. 208–218 (1999)

    Google Scholar 

  22. Thacker, R.A., Jones, K.R., Myers, C.J., Zheng, H.: Automatic abstraction for verification of cyber-physical systems. In: Proceedings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2010, pp. 12–21 (2010)

    Google Scholar 

  23. Yao, H., Zheng, H.: Automated interface refinement for compositional verification. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems 28(3), 433–446 (2009)

    Article  Google Scholar 

  24. Yoneda, T., Yoshikawa, T.: Using partial orders for trace theoretic verification of asynchronous circuits. In: Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems. IEEE Computer Society Press (March 1996)

    Google Scholar 

  25. Zheng, H.: Compositional reachability analysis for efficient modular verification of asynchronous designs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 29(3) (March 2010)

    Google Scholar 

  26. Zheng, H., Ahrens, J., Xia, T.: A compositional method with failure-preserving abstractions for asynchronous design verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 27 (2008)

    Google Scholar 

  27. Zheng, H., Mercer, E., Myers, C.: Modular verification of timed circuits using automatic abstraction. IEEE Transactions on Computer-Aided Design 22(9), 1138–1153 (2003)

    Article  Google Scholar 

  28. Zheng, H., Myers, C., Walter, D., Little, S., Yoneda, T.: Verification of timed circuits with failure directed abstractions. IEEE Transactions on Computer-Aided Design 25(3), 403–412 (2006)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of South Florida, Tampa, FL, 33620, USA

    Hao Zheng, Emmanuel Rodriguez & Yingying Zhang

  2. University of Utah, SLC, UT, 84112, USA

    Chris Myers

Authors
  1. Hao Zheng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Emmanuel Rodriguez
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yingying Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Chris Myers
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Imperial College London, 180 Queen’s Gate, SW7 2BZ, London, UK

    Alastair Donaldson

  2. School of Computer Science, University of Birmingham, B15 2TT, Edgbaston, Birmingham, UK

    David Parker

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zheng, H., Rodriguez, E., Zhang, Y., Myers, C. (2012). A Compositional Minimization Approach for Large Asynchronous Design Verification. In: Donaldson, A., Parker, D. (eds) Model Checking Software. SPIN 2012. Lecture Notes in Computer Science, vol 7385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31759-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31759-0_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31758-3

  • Online ISBN: 978-3-642-31759-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation