Skip to main content
SpringerLink
Log in

Efficient Verification of Timed Automata with BDD-Like Data-Structures

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2575))

Abstract

We investigate the efficiency of BDD-like data-structures for timed automata verification. We find that the efficiency is highly sensitive to the variable designs and canonical form definitions. We explore the two issues in details and propose to use CRD (Clock-Restriction Diagram) for timed automata state-space representation. We compare two canonical forms for zones, develop a procedure for quick zone-containment detection, and discuss the effect of variable-ordering of CRD. We implement our idea in our tool red 4.1 and carry out experiments to compare with other tools and red’s previous version in both forward and backward analysis.

The work is partially supported by NSC, Taiwan, ROC under grants NSC 90-2213- E-002-131, NSC 90-2213-E-002-132 Special thanks to Ms. Yu-Feng Chen, Mr. Geng-Dian Huang, and Mr. Fang Yu who helped collecting the huge set of experiment data.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
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. Asaraain, Bozga, Kerbrat, Maler, Pnueli, Rasse. Data-Structures for the Verification of Timed Automata. Proceedings, HART’97, LNCS 1201.

    Google Scholar 

  2. R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems. IEEE LICS, 1990.

    Google Scholar 

  3. F. Balarin. Approximate Reachability Analysis of Timed Automata. IEEE RTSS, 1996.

    Google Scholar 

  4. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. IEEE LICS, 1990.

    Google Scholar 

  5. M. Bozga, C. Daws. O. Maler. Kronos: A model-checking tool for real-time systems. 10th CAV, June/July 1998, LNCS 1427, Springer-Verlag.

    Google Scholar 

  6. J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, Wang Yi. UPPAAL-a Tool Suite for Automatic Verification of Real-Time Systems. Hybrid Control System Symposium, 1996, LNCS, Springer-Verlag.

    Google Scholar 

  7. G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, Wang Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. CAV’99, July, Trento, Italy, LNCS 1633, Springer-Verlag.

    Google Scholar 

  8. R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation, IEEE Trans. Comput., C-35(8), 1986.

    Google Scholar 

  9. D.L. Dill. Timing Assumptions and Verification of Finite-state Concurrent Systems. CAV’89, LNCS 407, Springer-Verlag.

    Google Scholar 

  10. T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine. Symbolic Model Checking for Real-Time Systems. IEEE LICS 1992.

    Google Scholar 

  11. K.G. Larsen, F. Larsson, P. Pettersson, Y. Wang. Efficient Verification of Real-Time Systems: Compact Data-Structure and State-Space Reduction. IEEE RTSS, 1998.

    Google Scholar 

  12. J. Moller, J. Lichtenberg, H.R. Andersen, H. Hulgaard. Difference Decision Diagrams. In proceedings of Annual Conference of the European Association for Computer Science Logic (CSL), Sept. 1999, Madrid, Spain.

    Google Scholar 

  13. J. Moller, J. Lichtenberg, H.R. Andersen, H. Hulgaard. Fully Symbolic Model-Checking of Timed Systems using Difference Decision Diagrams, In proceedings of Workshop on Symbolic Model-Checking (SMC), July 1999, Trento, Italy.

    Google Scholar 

  14. F. Wang. Efficient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems. TACAS’2000, March, Berlin, Germany; LNCS 1785, Springer-Verlag.

    Google Scholar 

  15. F. Wang. Region Encoding Diagram for Fully Symbolic Verification of Real-Time Systems. The 24th COMPSAC, Oct. 2000, Taipei, Taiwan, ROC, IEEE press.

    Google Scholar 

  16. F. Wang. RED: Model-checker for Timed Automata with Clock-Restriction Diagram. Workshop on Real-Time Tools, Aug. 2001, Technical Report 2001-014, ISSN 1404-3203, Dept. of Information Technology, Uppsala University.

    Google Scholar 

  17. F. Wang. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. In proceedings of FORTE’2001, Kluwer; August 2001, Cheju Island, Korea.

    Google Scholar 

  18. F. Wang, P.-A. Hsiung. fficient and User-Friendly Verification. IEEE Transactions on Computers, Jan. 2002.

    Google Scholar 

  19. F. Wang, A. Mok, E.A. Emerson. Symbolic Model-Checking for Distributed Real-Time Systems. In proceedings of 1st FME, April 1993, Denmark; LNCS 670, Springer-Verlag.

    Google Scholar 

  20. S. Yovine. Kronos: A Verification Tool for Real-Time Systems. International Journal of Software Tools for Technology Transfer, Vol. 1, Nr. 1/2, October 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Electrical Engineering, National Taiwan University, 1, Sec. 4, Roosevelt Rd., 106, Taipei, Taiwan, ROC

    Farn Wang

Authors
  1. Farn Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, New York University, 715 Broadway (7th floor), NY 10003, NewYork, USA

    Lenore D. Zuck

  2. College of Computer Science, Northeastern University, 360 Huntington Ave., 02115, Boston, MA, USA

    Paul C. Attie

  3. Computer Science Department, Venice University C’Foscari, Via Torino 155, 30170, Mestre-Venezia, Italy

    Agostino Cortesi

  4. Department of Computer Science and Electrical Engineering, West Virginia University, 26505, Morgantown, WV, USA

    Supratik Mukhopadhyay

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wang, F. (2003). Efficient Verification of Timed Automata with BDD-Like Data-Structures. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2003. Lecture Notes in Computer Science, vol 2575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36384-X_17

Download citation

  • DOI: https://doi.org/10.1007/3-540-36384-X_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00348-9

  • Online ISBN: 978-3-540-36384-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation