Skip to main content
SpringerLink
Log in

Symbolic Robustness Analysis of Timed Automata

  • Conference paper
Formal Modeling and Analysis of Timed Systems (FORMATS 2006)

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

Abstract

We propose a symbolic algorithm for the analysis of the robustness of timed automata, that is the correctness of the model in presence of small drifts on the clocks or imprecision in testing guards. This problem is known to be decidable with an algorithm based on detecting strongly connected components on the region graph, which, for complexity reasons, is not effective in practice.

Our symbolic algorithm is based on the standard algorithm for symbolic reachability analysis using zones to represent symbolic states and can then be easily integrated within tools for the verification of timed automata models. It relies on the computation of the stable zone of each cycle in a timed automaton. The stable zone is the largest set of states that can reach and be reached from itself through the cycle. To compute the robust reachable set, each stable zone that intersects the set of explored states has to be added to the set of states to be explored.

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. Altisen, K., Tripakis, S.: Implementation of timed automata: an issue of semantics or modeling? Technical report, Verimag, Centre Équation, 38610 Gières (June 2005)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  3. Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. 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. Daws, C.: Vérification de systèmes temporisés: de la théorie à la pratique. PhD thesis, Institut National Polytechnique de Grenoble (October 20, 1998)

    Google Scholar 

  6. Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  8. De Wulf, M., Doyen, L., Raskin, J.: Almost ASAP Semantics: from timed models to timed implementations (2004)

    Google Scholar 

  9. Gupta, V., Henzinger, T., Jagadeesan, R.: Robust Timed Automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 331–345. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  10. Larsen, K., Pettersson, P., Yi, W.: Uppaal in a nutshell. Software Tools for Technology Transfer 1(1+2), 134–152 (1997)

    Article  MATH  Google Scholar 

  11. Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for timed automata. In: LICS 2003: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, p. 198. IEEE Computer Society, Los Alamitos (2003)

    Chapter  Google Scholar 

  12. Puri, A.: Dynamical Properties of Timed Automata. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 210–227. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  13. Puri, A.: Dynamical Properties of Timed Automata. Discrete Event Dynamic Systems-Theory and Applications 10(1-2), 87–113 (2000)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Applied Mathematics,  

    Conrado Daws

  2. Formal Methods Group, Faculty of Electrical Engineering, Mathematics and Computer Science, University of Twente, The Netherlands

    Conrado Daws & Piotr Kordy

Authors
  1. Conrado Daws
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Piotr Kordy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LIAFA, CNRS and University Paris Diderot,  

    Eugene Asarin

  2. LSV, CNRS & ENS de Cachan, France

    Patricia Bouyer

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Daws, C., Kordy, P. (2006). Symbolic Robustness Analysis of Timed Automata. In: Asarin, E., Bouyer, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2006. Lecture Notes in Computer Science, vol 4202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11867340_11

Download citation

  • DOI: https://doi.org/10.1007/11867340_11

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45031-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation