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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
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.
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.
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.
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.
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.
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
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
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
DOI: https://doi.org/10.1007/978-3-030-12835-7_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-12834-0
Online ISBN: 978-3-030-12835-7
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)