Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2014: FM 2014: Formal Methods pp 351–366Cite as

A Symbolic Algorithm for the Analysis of Robust Timed Automata

  • Conference paper

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

Abstract

We propose an algorithm for the analysis of robustness of timed automata, that is, the correctness of a model in the presence of small drifts of the clocks. The algorithm is an extension of the region-based algorithm of Puri and uses the idea of stable zones as introduced by Daws and Kordy. Similarly to the assumptions made by Puri, we restrict our analysis to the class of timed automata with closed guards, progress cycles, and bounded clocks. We have implemented the algorithm and applied it to several benchmark specifications. The algorithm is a depth-first search based on on-the-fly reachability using zones.

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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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. Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Transactions on Programming Languages and Systems 16(5), 1543–1571 (1994)

    Article  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  3. Bengtsson, J.E., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Bouyer, P., Markey, N., Reynier, P.-A.: Robust model-checking of linear-time properties in timed automata. In: Correa, J.R., Hevia, A., Kiwi, M. (eds.) LATIN 2006. LNCS, vol. 3887, pp. 238–249. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Bouyer, P., Markey, N., Reynier, P.-A.: Robust analysis of timed automata via channel machines. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 157–171. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Bowman, H., Faconti, G., Katoen, J.-P., Latella, D., Massink, M.: Automatic verification of a lip-synchronisation protocol using uppaal. Formal Aspects of Computing 10(5-6), 550–575 (1998)

    Article  MATH  Google Scholar 

  7. 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 

  8. Daws, C., Kordy, P.: Symbolic robustness analysis of timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 143–155. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. 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 

  10. De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robustness and implementability of timed automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 118–133. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Formal Meth. Syst. Des. 33(1-3), 45–84 (2008)

    Article  MATH  Google Scholar 

  12. Dierks, H.: Comparing model checking and logical reasoning for real-time systems. Formal Asp. Comput. 16(2), 104–120 (2004)

    Article  MATH  Google Scholar 

  13. Dima, C.: Dynamical properties of timed automata revisited. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 130–146. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193–244 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  15. Jain, R.: FDDI Handbook: High-Speed Networking Using Fiber and Other Media. Addison Wesley Publishing Company (1994)

    Google Scholar 

  16. Jaubert, R., Reynier, P.-A.: Quantitative robustness analysis of flat timed automata. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 229–244. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  17. Department of Information Technology at Uppsala University and the Department of Computer Science at Aalborg University. UPPAAL, http://www.uppaal.org/

  18. Puri, A.: Dynamical properties of timed automata. Discrete Event Dynamic Systems-Theory and Applications 10(1-2), 87–113 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  19. Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing 1(2), 146–160 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  20. Wong-Toi, H.: Analysis of slope-parametric rectangular automata. In: Antsaklis, P.J., Kohn, W., Lemmon, M.D., Nerode, A., Sastry, S.S. (eds.) Hybrid Systems V 1997. LNCS, vol. 1567, pp. 390–413. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. Yannakakis, M., Lee, D.: An efficient algorithm for minimizing real-time transition systems. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 210–224. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  22. Yovine, S.: Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer 1, 123–133 (1997)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Twente, Drienerlolaan 5, 7522 NB, Enschede, The Netherlands

    Rom Langerak & Jan Willem Polderman

  2. Université du Luxembourg, rue Richard Coudenhove-Kalergi 6, L-1359, Luxembourg, Luxembourg

    Piotr Kordy & Sjouke Mauw

Authors
  1. Piotr Kordy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rom Langerak
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sjouke Mauw
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jan Willem Polderman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing Science, Newcastle University, NE1 7RU, Newcastle, UK

    Cliff Jones

  2. Data Abstraction (Pty) Ltd., 7 Saint David’s Park, Saint David’s Place, Parktown, Johannesburg, South Africa

    Pekka Pihlajasaari

  3. Information System Technology and Design, Singapore University of Technology and Design, 20 Dover Road, 138682, Singapore

    Jun Sun

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Kordy, P., Langerak, R., Mauw, S., Polderman, J.W. (2014). A Symbolic Algorithm for the Analysis of Robust Timed Automata. In: Jones, C., Pihlajasaari, P., Sun, J. (eds) FM 2014: Formal Methods. FM 2014. Lecture Notes in Computer Science, vol 8442. Springer, Cham. https://doi.org/10.1007/978-3-319-06410-9_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-06410-9_25

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-06409-3

  • Online ISBN: 978-3-319-06410-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation