Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Modeling and Analysis of Timed Systems

FORMATS 2012: Formal Modeling and Analysis of Timed Systems pp 91–106Cite as

Multi-core Reachability for Timed Automata

  • Conference paper

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

Abstract

Model checking of timed automata is a widely used technique. But in order to take advantage of modern hardware, the algorithms need to be parallelized. We present a multi-core reachability algorithm for the more general class of well-structured transition systems, and an implementation for timed automata.

Our implementation extends the opaal tool to generate a timed automaton successor generator in c++, that is efficient enough to compete with the uppaal model checker, and can be used by the discrete model checker LTSmin, whose parallel reachability algorithms are now extended to handle subsumption of semi-symbolic states. The reuse of efficient lockless data structures guarantees high scalability and efficient memory use.

With experiments we show that opaal+LTSmin can outperform the current state-of-the-art, uppaal. The added parallelism is shown to reduce verification times from minutes to mere seconds with speedups of up to 40 on a 48-core machine. Finally, strict BFS and (surprisingly) parallel DFS search order are shown to reduce the state count, and improve speedups.

This is a preview of subscription content, 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   49.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General Decidability Theorems for Infinite-State Systems. In: Proceedings of Eleventh Annual IEEE Symposium on Logic in Computer Science, LICS 1996, pp. 313–321 (July 1996)

    Google Scholar 

  2. Agarwal, V., Petrini, F., Pasetto, D., Bader, D.A.: Scalable Graph Exploration on Multicore Processors. In: Proceedings of the 2010 ACM/IEEE International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2011, pp. 1–11. IEEE Computer Society, Washington, DC (2010)

    Google Scholar 

  3. Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  4. Amnell, T., Behrmann, G., Bengtsson, J.E., D’Argenio, P.R., David, A., Fehnker, A., Hune, T., Jeannet, B., Larsen, K.G., Möller, M.O., Pettersson, P., Weise, C., Yi, W.: UPPAAL - Now, Next, and Future. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 99–124. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Barnat, J., Ročkai, P.: Shared Hash Tables in Parallel Model Checking. Electronic Notes in Theoretical Computer Science 198(1), 79–91 (2007); Proceedings of PDMC 2007

    Article  Google Scholar 

  6. Behrmann, G.: Distributed Reachability Analysis in Timed Automata. International Journal on Software Tools for Technology Transfer 7(1), 19–30 (2005)

    Article  Google Scholar 

  7. Behrmann, G., Bengtsson, J.E., David, A., Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL Implementation Secrets. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 3–22. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static Guard Analysis in Timed Automata Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–270. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing Uppaal over 15 years. Software: Practice and Experience 41(2), 133–142 (2011)

    Article  Google Scholar 

  11. Behrmann, G., Hune, T., Vaandrager, F.: Distributing Timed Model Checking - How the Search Order Matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  12. Bengtsson, J.: Clocks, DBMs and states in timed systems. PhD thesis, Uppsala University (2002)

    Google Scholar 

  13. Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and Symbolic Reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods in System Design 24(3), 281–320 (2004)

    Article  MATH  Google Scholar 

  15. Braberman, V., Olivero, A., Schapachnik, F.: Dealing with practical limitations of distributed timed model checking for timed automata. Formal Methods in System Design 29, 197–214 (2006), doi:10.1007/s10703-006-0012-3

    Article  MATH  Google Scholar 

  16. Comon, H., Jurski, Y.: Timed Automata and the Theory of Real Numbers. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 242–257. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Dalsgaard, A.E., Hansen, R.R., Jørgensen, K.Y., Larsen, K.G., Olesen, M.C., Olsen, P., Srba, J.: opaal: A Lattice Model Checker. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 487–493. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  18. Evangelista, S., Laarman, A., Petrucci, L., van de Pol, J.: Improved Multi-Core Nested Depth-First Search. In: Mukund, M., Chakraborty, S. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 269–283. Springer, Heidelberg (2012)

    Google Scholar 

  19. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  20. Laarman, A., Langerak, R., van de Pol, J., Weber, M., Wijs, A.: Multi-core Nested Depth-First Search. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 321–335. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  21. Laarman, A.W., van de Pol, J.: Variations on Multi-Core Nested Depth-First Search. In: Barnat, J., Heljanko, K. (eds.) PDMC. EPTCS, vol. 72, pp. 13–28 (2011)

    Google Scholar 

  22. Laarman, A.W., van de Pol, J., Weber, M.: Boosting Multi-Core Reachability Performance with Shared Hash Tables. In: Sharygina, N., Bloem, R. (eds.) Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design, Lugano, Swiss. IEEE Computer Society (October 2010)

    Google Scholar 

  23. Laarman, A., van de Pol, J., Weber, M.: Multi-Core LTSmin: Marrying Modularity and Scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506–511. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Laarman, A., van de Pol, J., Weber, M.: Parallel Recursive State Compression for Free. In: Groce, A., Musuvathi, M. (eds.) SPIN Workshops 2011. LNCS, vol. 6823, pp. 38–56. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  25. Sanders, P.: Lastverteilungsalgorithmen fur Parallele Tiefensuche. number 463. In: Fortschrittsberichte, Reihe 10. VDI. Verlag (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Formal Methods and Tools, University of Twente, The Netherlands

    Alfons Laarman & Jaco van de Pol

  2. Department of Computer Science, Aalborg University, Denmark

    Andreas E. Dalsgaard, Kim G. Larsen & Mads Chr. Olesen

Authors
  1. Andreas E. Dalsgaard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alfons Laarman
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mads Chr. Olesen
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Warwick, CV4 7AL, Coventry, UK

    Marcin Jurdziński

  2. Business Unit Safe and Autonomous Systems, Department of Safety and Security, AIT Austrian Institute of Technology, Donau-City-Str. 1, 1220, Vienna, Austria

    Dejan Ničković

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dalsgaard, A.E., Laarman, A., Larsen, K.G., Olesen, M.C., van de Pol, J. (2012). Multi-core Reachability for Timed Automata. In: Jurdziński, M., Ničković, D. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2012. Lecture Notes in Computer Science, vol 7595. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33365-1_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33365-1_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33364-4

  • Online ISBN: 978-3-642-33365-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation