Quantitative Analysis of Real-Time Systems Using Priced Timed Automata

Article, Review English OPEN
Bouyer, Patricia ; Fahrenberg, Uli ; Larsen, Kim G. ; Markey, Nicolas (2011)
  • Journal: COMMUNICATIONS OF THE ACM (issn: 0001-0782)
  • Related identifiers: doi: 10.1145/1995376.1995396
  • Subject: [ INFO ] Computer Science [cs] | [ INFO.INFO-FL ] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]

International audience; The problems of time-dependent behavior in general, and dynamic resource allocation in particular, pervade many aspects of modern life. Prominent examples range from reliability and efficient use of communication resources in a telecommunication network to the allocation of tracks in a continental railway network, from scheduling the usage of computational resources on a chip for durations of nanoseconds to the weekly, monthly or longer-range reactive planning in a factory or a supply chain. These problems have been subject to substantial research for decades by different communities such as operational research, computer systems performance evaluation as well as planning and scheduling, witnessed by large ACM communities such as SIGMETRICS and PERFORMANCE. In this paper we argue that the formalism of timed automata together with recent extensions provides an alternative framework with complementary, yet competitive, results in terms of modeling ca-pabilities and efficiency of analysis.
  • References (29)
    29 references, page 1 of 3

    6. REFERENCES automata with energy constraints. In Proc. 6th

    [1] Y. Abdeddaïm, E. Asarin, and O. Maler. International Conference on Formal Modeling Scheduling with timed automata. Theoretical and Analysis of Timed Systems (FORMATS'08), Computer Science, 354(2):272-300, 2006. Lecture Notes in Computer Science, Lecture

    [2] K. Altisen et al. A framework for scheduler syn- Notes in Computer Science. Springer, 2008. thesis. In IEEE Real-Time Systems Symposium, [15] P. Bouyer et al. Almost optimal strategies p. 154-163, 1999. in one-clock priced timed automata. In Proc.

    [3] R. Alur, M. Bernadsky, and P. Madhusu- 26th Conference on Foundations of Software dan. Optimal reachability in weighted timed Technology and Theoretical Computer Science games. In Proc. 31st International Colloquium (FSTTCS'06), Lecture Notes in Computer Scion Automata, Languages and Programming ence 4337, p. 345-356. Springer, 2006. (ICALP'04), Lecture Notes in Computer Science [16] M. Bozga et al. Verification of asynchronous cir3142, p. 122-133. Springer, 2004. cuits using timed automata. Electronic Notes in

    [4] R. Alur, C. Courcoubetis, and D. L. Dill. Model- Theoretical Computer Science, 65(6), 2002. checking for real-time systems. In Proc. 5th An- [17] Th. Brihaye, V. Bruyère, and J.-F. Raskin. On opnual Symposium on Logic in Computer Science timal timed strategies. In Proc. 3rd International (LICS'90), p. 414-425. IEEE Computer Society Conference on Formal Modeling and Analysis of Press, 1990. Timed Systems (FORMATS'05), Lecture Notes

    [5] R. Alur and D. L. Dill. Automata for modeling in Computer Science 3821, p. 49-64. Springer, real-time systems. In Proc. 17th International 2005. Colloquium on Automata, Languages and Pro- [18] F. Cassez et al. Efficient on-the-fly algorithms gramming (ICALP'90), Lecture Notes in Com- for the analysis of timed games. In Proc. 16th Inputer Science 443, p. 322-335. Springer, 1990. ternational Conference on Concurrency Theory

    [6] R. Alur, S. La Torre, and G. J. Pappas. Opti- (CONCUR'05), Lecture Notes in Computer Scimal paths in weighted timed automata. In Proc. ence 3653, p. 66-80. Springer, 2005. 4th International Workshop on Hybrid Systems: [19] F. Cassez et al. Timed control with observaComputation and Control (HSCC'01), Lecture tion based and stuttering invariant strategies. Notes in Computer Science 2034, p. 49-62. In Proc. 5th International Symposium on AutoSpringer, 2001. mated Technology for Verification and Analysis

    [7] E. Asarin and O. Maler. As soon as possi- (ATVA'07), Lecture Notes in Computer Science ble: Time optimal control for timed automata. 4762, p. 192-206. Springer, 2007. In Proc. 2nd International Workshop on Hybrid [20] F. Cassez et al. Automatic synthesis of robust Systems: Computation and Control (HSCC'99), and optimal controllers - an industrial case Lecture Notes in Computer Science 1569, p. 19- study. In Proc. 12th International Workshop 30. Springer, 1999. on Hybrid Systems: Computation and Control

    [8] E. Asarin et al. Controller synthesis for timed (HSCC'09), Lecture Notes in Computer Science automata. In Proc. IFAC Symposium on System 5469. Springer, 2009. Structure and Control, p. 469-474. Elsevier Sci- [21] A. Chakrabarti et al. Resource interfaces. In ence, 1998. Proc. 3rd International Workshop on Embedded

    [9] G. Behrmann et al. Efficient guiding towards Software (EMSOFT'03), Lecture Notes in Comcost-optimality in UPPAAL. In Proc. 7th Inter- puter Science 2855. Springer, January 2003. national Conference on Tools and Algorithms [22] A. David et al. Model-based framework for for the Construction and Analysis of Systems schedulability analysis using UPPAAL 4.1. In (TACAS'01), Lecture Notes in Computer Sci- G. Nicolescu and P. J. Mosterman, editors, ence 2031, p. 174-188. Springer, 2001. Model-Based Design for Embedded Systems,

  • Metrics
    No metrics available
Share - Bookmark