Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

The Surprising Robustness of (Closed) Timed Automata against Clock-Drift

  • Conference paper

We investigate reachability (or equivalently, safety) for timed systems modelled as Timed Automata (TA) under notions of “robustness”, i.e., when the clocks of the TA may drift by small amounts. Our contributions are two-fold: (1) We first consider the model of clock-drift introduced by Puri [1] and subsequently studied in other works [2,3,4]. We show that the standard zone-based forward reachability analysis performed by tools such as UPPAAL is in fact exact for TA with closed guards, invariants, and targets, when testing robust safety of timed systems having an arbitrary, but finite lifetime. (2) Next, we consider a more realistic model of drifting clocks that takes into account the regular resynchronization performed in most practical systems. We then show that the standard reachability analysis of tools like UPPAAL again suffices to test for robust safety in this model of clock-drift, for TA with closed guards, invariants, and targets, but now without any restrictions on system life-time.

Similar content being viewed by others

Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. A. Puri, “Dynamical Properties of Timed Automata”,Discrete Event Dynamic Systems10, Kluwer (2000), 87–113

    Article MathSciNet MATH  Google Scholar 

  2. M. de Wulf, L. Doyen, N. Markey, and J.-F. Raskin, “Robustness and Implementability of Timed Automata”,Proc. of FORMATS-FTRTFT’04, LNCS3253, Springer (2004), 118-133

    Google Scholar 

  3. C. Daws and P. Kordy, “Symbolic Robustness Analysis of Timed Automata”,Proc. of FORMATS’06, LNCS4202, Springer (2006), 143-155

    Google Scholar 

  4. C. Dima, “Dynamical Properties of Timed Automata Revisited”,Proc. of FORMATS’07, LNCS4763, Springer (2007), 130–146

    Google Scholar 

  5. R. Alur and D. Dill, “A Theory of Timed Automata”,Theoretical Computer Science126, Elsevier (1994), 183–235

    Article MathSciNet MATH  Google Scholar 

  6. G. Behrmann, A. David, and K. Larsen, “A Tutorial on Uppaal”,Formal Methods for the Design of Real-Time Systems, LNCS3185, Springer-Verlag (2004), 200–236

    MATH  Google Scholar 

  7. M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, S. Yovine, “KRONOS: A Model-Checking Tool for Real-Time Systems”,Proc. of FTRTFT’98, LNCS1486, Springer (1998), 298–302

    Google Scholar 

  8. M. Lindahl, P. Pettersson, and W. Yi, “Formal Design and Analysis of a Gear Controller”,International Journal on Software Tools for Technology Transfer3, Springer-Verlag (2001), 353–368

    MATH  Google Scholar 

  9. L. Aceto, P. Bouyer, A. Burgueno, and K. Larsen, “The Power of Reachability Testing for Timed Automata”,Theoretical Computer Science300, Elsevier (2003), 411-475

    Article MathSciNet MATH  Google Scholar 

  10. J. Bengtsson and W. Yi, “Timed Automata: Semantics, Algorithms, and Tools”,Lectures on Concurrency and Petri Nets, LNCS3098, Springer (2004), 87–124

    MATH  Google Scholar 

  11. P. Bouyer, “Forward Analysis of Updatable Timed Automata”,Formal Methods in System Design24, Kluwer (2004), 281–320

    Article MATH  Google Scholar 

  12. M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, “Automatic Verification of Real-time Systems with Discrete Probability Distributions”,Theoretical Computer Science282, Elsevier (2002), 101-150

    Article MathSciNet MATH  Google Scholar 

  13. V. Gupta, T. A. Henzinger, and R. Jagadeesan, “Robust Timed Automata”,Proc. of HART’97, LNCS1201, Springer (1997), 331–345

    Google Scholar 

  14. J. Ouaknine and J. Worrell, “Revisiting Digitization, Robustness, and Decidability for Timed Automata”,Proc. of LICS’03, IEEE CS Press (2003), 198-207

    Google Scholar 

  15. P. Bouyer, N. Markey, and P.-A. Reynier, “Robust Model-Checking of Linear-Time Properties in Timed Automata”,Proc. of LATIN’06, LNCS3887, Springer (2006), 238–249.

    Google Scholar 

  16. P. Bouyer, N. Markey, and P.-A. Reynier, “Robust Analysis of Timed Automata via Channel Machines”,Proc. of FoSSaCS’08, LNCS4962, Springer (2008), 157-171

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oldenburg, Oldenburg, Germany

    Mani Swaminathan & Martin Fränzle

  2. ASKON Consulting Group GmbH, GmbH, Germany

    Mani Swaminathan

  3. RWTH Aachen University, Aachen, Germany

    Joost-Pieter Katoen

Authors
  1. Mani Swaminathan

    You can also search for this author inPubMed Google Scholar

  2. Martin Fränzle

    You can also search for this author inPubMed Google Scholar

  3. Joost-Pieter Katoen

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Rome, Italy

    Giorgio Ausiello

  2. University of Turku, Finland

    Juhani Karhumäki

  3. University of Milano, Italy

    Giancarlo Mauri

  4. Cambridge University, United Kingdom

    Luke Ong

Rights and permissions

Copyright information

© 2008 IFIP International Federation for Information Processing

About this paper

Cite this paper

Swaminathan, M., Fränzle, M., Katoen, JP. (2008). The Surprising Robustness of (Closed) Timed Automata against Clock-Drift. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds) Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008. IFIP International Federation for Information Processing, vol 273. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-09680-3_36

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp