Skip to main content
SpringerLink
Log in

Timed IMDS

  • Chapter
  • First Online:
Book cover Integrated Model of Distributed Systems

Part of the book series: Studies in Computational Intelligence ((SCI,volume 817))

Abstract

The behavior of a distributed system may depend on real time flow (as opposed to succession of events in discrete systems), because changes in the system may take some time. As a result, deadlock situations may depend on relations between periods of time associated with individual changes.

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 84.99
Price excludes VAT (USA)
  • Available as EPUB and 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
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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

References

  • Alur, R., & Dill, D. L. (1994). A theory of timed automata. Theoretical Computer Science, 126(2), 183–235. https://doi.org/10.1016/0304-3975(94)90010-8.

    Article  MathSciNet  MATH  Google Scholar 

  • Behrmann, G., Cougnard, A., David, A., Fleury, E., Gulstrand Larsen, K., & Lime, D. (2006). Uppaal-Tiga: Timed games for everyone. In Nordic Workshop on Programming Theory (NWPT’06), Reykjavik, Iceland, October 18–20, 2006. URL: https://hal.archives-ouvertes.fr/hal-00350470/document.

  • Behrmann, G., David, A., & Larsen, K. G. (2006). A tutorial on Uppaal 4.0. Aalborg, Denmark. URL: http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf.

  • Benghazi Akhlaki, K., Capel Tuñón, M. I., Holgado Terriza, J. A., & Mendoza Morales L E. (2007). A methodological approach to the formal specification of real-time systems by transformation of UML-RT design models. Science of Computer Programming, 65(1), 41–56. https://doi.org/10.1016/j.scico.2006.08.005.

  • Bérard, B. (2013). An introduction to timed automata. In Control of discrete-event systems (pp. 169–187). London, UK: Springer. https://doi.org/10.1007/978-1-4471-4276-8_9.

  • Bérard, B., Cassez, F., Haddad, S., Lime, D., & Roux, O. H. (2005). Comparison of the expressiveness of timed automata and time Petri nets. In Third International Conference FORMATS 2005, Uppsala, Sweden (pp. 211–225), September 26–28, 2005. Berlin: Springer. https://doi.org/10.1007/11603009_17.

  • Bowman, H. (2001). Time and action lock freedom properties for timed automata. In 21st International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2001, Cheju Island, Korea (pp. 119–134), August 28–31, 2001. Boston: Kluwer Academic Publishers. https://doi.org/10.1007/0-306-47003-9_8.

  • Bowman, H., Gomez, R., & Su, L. (2005). A tool for the syntactic detection of zeno-timelocks in timed automata. Electronic Notes in Theoretical Computer Science, 139(1), 25–47. https://doi.org/10.1016/j.entcs.2005.09.006.

    Article  MATH  Google Scholar 

  • Cassez, F., & Roux, O. H. (2006). Structural translation from time Petri nets to timed automata. Journal of Systems and Software, 79(10), 1456–1468. https://doi.org/10.1016/j.jss.2005.12.021.

    Article  MATH  Google Scholar 

  • Emerson, E. A., Mok, A. K., Sistla, P., & Srinivasan, J. (1992). Quantitative temporal reasoning. Real-Time Systems, 4(4), 331–352. https://doi.org/10.1007/bf00355298.

  • Frossl, J., Gerlach, J, & Kropf, T. (1996). An efficient algorithm for real-time symbolic model checking. In Proceedings ED&TC European Design and Test Conference, Paris, France (pp. 15–20), March 11–14, 1996. New York, NY: IEEE Computer Society Press. https://doi.org/10.1109/edtc.1996.494120.

  • Gluchowski, P. (2009). Languages of CTL and RTCTL Calculi in real-time analysis of a system described by a fault tree with time dependencies. In 2009 Fourth International Conference on Dependability of Computer Systems, DepCoS–RELCOMEX ’09, Brunów, Poland (pp. 33–41), June 30–July 2, 2009. New York, NY: IEEE. https://doi.org/10.1109/depcos-relcomex.2009.12.

  • Gómez, R., & Bowman, H. (2007). Efficient detection of zeno runs in timed automata. In 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2007), Salzburg, Austria (pp. 195–210), October 3–5, 2007, LNCS 4763. Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-540-75454-1_15.

  • Hadjidj, R., Boucheneb, H., & Hadjidj, D. (2007). Zenoness detection and timed model checking for real time systems. In K. Barkaoui & M. Ioualalen (Eds.), First International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS’07), Algiers, Algeria (pp. 120–134), May 5–6, 2007. Swinton, UK: British Computer Society. url: https://www.bcs.org/upload/pdf/ewic_ve07_s3paper3.pdf.

  • Holzmann, G. J. (1995). Tutorial: Proving properties of concurrent systems with SPIN. In 6th International Conference on Concurrency Theory (CONCUR’95, Philadelphia, PA) (pp. 453–455), August 21–24, 1995. Berlin, Heidelberg: Springer. https://doi.org/10.1007/3-540-60218-6_34.

  • Krystosik, A., & Turlej, D. (2006). EMLAN: A language for model checking of embedded systems software. In IFAC Workshop on Programmable Devices and Embedded Systems, Brno, Czech Republic (pp. 126–131), February 14–16, 2006. Amsterdam: Elsevier Science. https://doi.org/10.1016/S1474-6670(17)30171-4

  • Lime, D., & Roux, O. H. (2006). Model checking of time petri nets using the state class timed automaton. Discrete Event Dynamic Systems, 16(2), 179–205. https://doi.org/10.1007/s10626-006-8133-9.

    Article  MathSciNet  MATH  Google Scholar 

  • Lindahl, M., Pettersson, P., & Yi, W. (2001). Formal design and analysis of a gear controller. International Journal on Software Tools for Technology Transfer, 3, 353–368. https://doi.org/10.1007/s100090100048.

  • Popescu, C., & Martinez Lastra, J. L. (2010). Formal methods in factory automation. In J. Silvestre-Blanes (Ed.), Factory automation (pp. 463–475). Rijeka, Croatia: InTech. https://doi.org/10.5772/9526.

  • Ruf, J., & Kropf, T. (2003). Symbolic verification and analysis of discrete timed systems. Formal Methods in System Design, 23(1), 67–108. https://doi.org/10.1023/A:1024437214071.

    Article  MATH  Google Scholar 

  • Winskel, G., & Nielsen, M. (1995). Models for concurrency. In S. Abramsky, D. M. Gabbay, & T. S. E. Maibaum (Eds.), Handbook of logic in computer science (Vol. 4, pp. 1–148). Oxford, UK: Oxford University Press. ISBN: 0-19-853780-8

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Warsaw University of Technology, Warsaw, Poland

    Wiktor B. Daszczuk

Authors
  1. Wiktor B. Daszczuk
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wiktor B. Daszczuk .

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Daszczuk, W.B. (2020). Timed IMDS. In: Integrated Model of Distributed Systems. Studies in Computational Intelligence, vol 817. Springer, Cham. https://doi.org/10.1007/978-3-030-12835-7_10

Download citation

Publish with us

Policies and ethics

Search

Navigation