Skip to main content
SpringerLink
Log in

Parametric Deadlock-Freeness Checking Timed Automata

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2016 (ICTAC 2016)

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

Included in the following conference series:

Abstract

Distributed real-time systems are notoriously difficult to design, and must be verified, e. g., using model checking. In particular, deadlocks must be avoided as they either yield a system subject to potential blocking, or denote an ill-formed model. Timed automata are a powerful formalism to model and verify distributed systems with timing constraints. In this work, we investigate synthesis of timing constants in timed automata for which the model is guaranteed to be deadlock-free.

This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002).

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

Notes

  1. 1.

    Experiments were conducted on Linux Mint 17 64 bits, running on a Dell Intel Core i7 CPU 2.67 GHz with 4 GiB. Binaries, models and results are available at www.imitator.fr/static/ICTAC16/.

  2. 2.

    The synchronous product of several PTA components (using synchronized actions) yields a PTA. IMITATOR performs this composition on-the-fly.

References

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  3. André, É., Fribourg, L., Kühne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33–36. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32759-9_6

    Chapter  Google Scholar 

  4. André, É., Lime, D.: Liveness in L/U-parametric timed automata (2016, submitted). https://hal.archives-ouvertes.fr/hal-01304232

  5. Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)

    Article  MathSciNet  Google Scholar 

  6. Beneš, N., Bezděk, P., Larsen, K.G., Srba, J.: Language emptiness of continuous-time parametric timed automata. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 69–81. Springer, Heidelberg (2015). doi:10.1007/978-3-662-47666-6_6

    Google Scholar 

  7. Clarisó, R., Cortadella, J.: Verification of concurrent systems with parametric delays using octahedra. In: ACSD, pp. 122–131. IEEE Computer Society (2005)

    Google Scholar 

  8. Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. JLAP 52–53, 183–220 (2002)

    MathSciNet  MATH  Google Scholar 

  9. Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. IEEE Trans. Softw. Eng. 41(5), 445–461 (2015)

    Article  MATH  Google Scholar 

  10. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)

    Article  MATH  Google Scholar 

  11. Markey, N.: Robustness in real-time systems. In: SIES, pp. 28–34. IEEE Computer Society Press (2011)

    Google Scholar 

  12. 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). doi:10.1007/978-3-642-02658-4_59

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France

    Étienne André

  2. École Centrale de Nantes, IRCCyN, CNRS, UMR 6597, Nantes, France

    Étienne André

Authors
  1. Étienne André
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Étienne André .

Editor information

Editors and Affiliations

  1. Universidade Federal de Pernambuco Centro de Informática, Recife, Pernambuco, Brazil

    Augusto Sampaio

  2. Deptartment of Electrical Engineering BL, National Taiwan University, Taipei, Taiwan

    Farn Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

André, É. (2016). Parametric Deadlock-Freeness Checking Timed Automata. In: Sampaio, A., Wang, F. (eds) Theoretical Aspects of Computing – ICTAC 2016. ICTAC 2016. Lecture Notes in Computer Science(), vol 9965. Springer, Cham. https://doi.org/10.1007/978-3-319-46750-4_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46750-4_27

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46749-8

  • Online ISBN: 978-3-319-46750-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation