Skip to main content
SpringerLink
Log in

Scaling BDD-based Timed Verification with Simulation Reduction

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10009))

Included in the following conference series:

  • 821 Accesses

Abstract

Digitization is a technique that has been widely used in real-time model checking. With the assumption of digital clocks, symbolic model checking techniques (like those based on BDDs) can be applied for real-time systems. The problem of model checking real-time systems based on digitization is that the number of tick transitions increases rapidly with the increment of clock upper bounds. In this paper, we propose to improve BDD-based verification for real-time systems using simulation reduction. We show that simulation reduction allows us to verify timed automata with large clock upper bounds and to converge faster to the fixpoint. The presented approach is applied to reachability and LTL verification for real-time systems. Finally, we compare our approach with existing tools such as Rabbit, Uppaal, and CTAV and show that our approach outperforms them and achieves a significant speedup.

This work is supported by research project T2MOE1303.

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 EPUB and 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

References

  1. MCMT Benchmarks of Timed Automata. http://crema.di.unimi.it/~carioni/mcmt_ta.html

  2. Technical Report of Scaling BDD-based Timed Verification with Simulation Reduction. http://tianhuat.github.io/tr_bddsr.pdf

  3. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592–601 (1993)

    Google Scholar 

  5. Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 470–484. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  6. Aziz, A., Tasiran, S., Brayton, R.K.: BDD variable ordering for interacting finite state machines. In: DAC, pp. 283–288 (1994)

    Google Scholar 

  7. Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 312–326. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  8. Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  9. Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 318–343. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  10. Beyer, D., Lewerentz, C., Noack, A.: Rabbit: a tool for BDD-based verification of real-time systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 122–125. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Beyer, D., Noack, A.: Efficient verification of timed automata using BDDs. In: FMICS, pp. 95–113 (2001)

    Google Scholar 

  12. Beyer, D., Noack, A.: Can decision diagrams overcome state space explosion in real- time verification. In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 193–208. Springer, Heidelberg (2003)

    Google Scholar 

  13. Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods Syst. Des. 24(3), 281–320 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  14. Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Vardi, Y.M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)

    Google Scholar 

  15. Bozga, M., Maler, O., Pnueli, A., Yovine, S.: Some progress in the symbolic verification of timed automata. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 179–190. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  16. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  17. Chen, M., Tan, T.H., Sun, J., Liu, Y., Pang, J., Li, X.: Verification of functional and non-functional requirements of web service composition. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 313–328. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  18. Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 277–293. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  19. Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  20. Sifakis, J.: Timing assumptions and verification of finite-state concurrent systems. In: Dill, D.L. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1989)

    Google Scholar 

  21. Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation preorders. In: Larsen, K.G., Hu, A.J., Wong-Toi, H. (eds.) CAV 1991. LNCS, vol. 575, pp. 255–265. Springer, Heidelberg (1991)

    Google Scholar 

  22. Doyen, L., Raskin, J.-F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 2–22. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  23. Fujii, H., Ootomo, G., Hori, C.: Interleaving based variable ordering methods for ordered binary decision diagrams. In: ICCAD, pp. 38–41 (1993)

    Google Scholar 

  24. Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)

    Google Scholar 

  25. Herbreteau, F., Srivathsan, B.: Efficient on-the-fly emptiness check for timed Büchi automata. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 218–232. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  26. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient emptiness check for timed Büchi automata. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 148–161. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  27. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Better abstractions for timed automata. In: LICS, pp. 375–384 (2012)

    Google Scholar 

  28. Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 1–16. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  29. Laarman, A., Olesen, M.C., Dalsgaard, A.E., Larsen, K.G., van de Pol, J.: Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 968–983. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  30. Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  31. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. STTT 1(1–2), 134–152 (1997)

    Article  MATH  Google Scholar 

  32. Li, G.: Checking timed Büchi automata emptiness using LU-abstractions. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 228–242. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  33. Li, Y., Tan, T.H., Chechik, M.: Management of time requirements in component-based systems. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 399–415. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  34. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  35. Møller, J.B., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference decision diagrams. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 111–125. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  36. Morbé, G., Pigorsch, F., Scholl, C.: Fully symbolic model checking for timed automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 616–632. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  37. Nguyen, T.K., Sun, J., Liu, Y., Dong, J.S., Liu, Y.: Improved BDD-based discrete analysis of timed systems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 326–340. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  38. Rice, M., Kulhari, S.: A survey of static variable ordering heuristics for efficient BDD/MDD construction. Technical report, University of California, Riverside (2008)

    Google Scholar 

  39. Rozier, K.Y.: Linear temporal logic symbolic model checking. Comput. Sci. Rev. 5(2), 163–203 (2011)

    Article  MATH  Google Scholar 

  40. Seshia, S.A., Bryant, R.E.: Unbounded, fully symbolic model checking of timed automata using Boolean methods. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 154–166. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  41. Somenzi, F.: CUDD: CU Decision Diagram Package. http://vlsi.colorado.edu/~fabio/CUDD/

  42. Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  43. Tan, T.H., Liu, Y., Sun, J., Dong, J.S.: Verification of orchestration systems using compositional partial order reduction. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 98–114. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  44. Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 299–314. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  45. Tripakis, S.: Checking timed Büchi automata emptiness on simulation graphs. ACM Trans. Comput. Logic 10(3), 1–19 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  46. Wang, F.: Symbolic verification of complex real-time systems with clock-restriction diagram. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) FORTE 2001, vol. 69, pp. 235–250. Springer, Heidelberg (2001)

    Google Scholar 

  47. Wang, F.: Efficient verification of timed automata with BDD-like data-structures. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 189–205. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Autodesk, San Rafael, USA

    Truong Khanh Nguyen

  2. Singapore University of Technology and Design, Singapore, Singapore

    Tian Huat Tan, Jun Sun, Jiaying Li & Manman Chen

  3. Nanyang Technological University, Singapore, Singapore

    Yang Liu

  4. National University of Singapore, Singapore, Singapore

    Jin Song Dong

Authors
  1. Truong Khanh Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tian Huat Tan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jun Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jiaying Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Yang Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Manman Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Jin Song Dong
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jiaying Li .

Editor information

Editors and Affiliations

  1. School of Information Science, Japan Advanced Institute of Science and Technology (JAIST), Nomi, Japan

    Kazuhiro Ogata

  2. Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada

    Mark Lawford

  3. Department of Computer Science, Hosei University, Tokyo, Japan

    Shaoying Liu

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Nguyen, T.K. et al. (2016). Scaling BDD-based Timed Verification with Simulation Reduction. In: Ogata, K., Lawford, M., Liu, S. (eds) Formal Methods and Software Engineering. ICFEM 2016. Lecture Notes in Computer Science(), vol 10009. Springer, Cham. https://doi.org/10.1007/978-3-319-47846-3_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47846-3_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47845-6

  • Online ISBN: 978-3-319-47846-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation