A survey of timed automata for the development of real-time systems

Alur, 1990, Automata for modeling real-time systems, 322 Alur, 1994, A theory of timed automata, Theoretical Computer Science, 126, 183, 10.1016/0304-3975(94)90010-8 Henzinger, 1994, Symbolic model checking for real-time systems, Information and Computation, 111, 394, 10.1006/inco.1994.1045 Alur, 1999, Timed automata, Theoretical Computer Science, 126, 183, 10.1016/0304-3975(94)90010-8 Bérard, 1998, Characterization of the expressive power of silent transitions in timed automata, Fundamenta Informaticae, 36, 145, 10.3233/FI-1998-36233 Alur, 1993, Model-checking in dense real-time, Information and Computation, 104, 2, 10.1006/inco.1993.1024 Fersman, 2002, Timed automata with asynchronous processes: Schedulability and decidability, 67 Alur, 1992, Minimization of timed transition systems, 340 Tripakis, 2001, Analysis of timed systems using time-abstracting bisimulations, Formal Methods in System Design, 18, 25, 10.1023/A:1008734703554 Dill, 1990, Timing assumptions and verification of finite-state concurrent systems, 197 Puri, 1998, Dynamical properties of timed automata, 210 M. Sorea, Verification of real-time systems through lazy approximations, Ph.D. Thesis, Universität Ulm, Germany, 2003. Behrmann, 2011, Developing UPPAAL over 15 years, Software: Practice and Experience, 41, 133, 10.1002/spe.1006 Daws, 1996, The tool KRONOS, 208 Bellman, 1957 J. Bengtsson, Clocks, DBMs and states in timed systems. Ph.D. Thesis, Department of Information Technology, Uppsala University, Uppsala, Sweden, 2002. Bengtsson, 2004, Timed automata: semantics, algorithms and tools, vol. 3098 Daws, 1998, Model checking of real-time reachability properties using abstractions, 313 Bouajjani, 1997, On-the-fly symbolic model checking for real-time systems, 232 Tripakis, 2005, Checking timed Büchi automata emptiness efficiently, Formal Methods in System Design, 26, 267, 10.1007/s10703-005-1632-8 Tripakis, 2009, Checking timed Büchi automata emptiness on simulation graphs, ACM Transactions on Computational Logic, 10, 10.1145/1507244.1507245 T.G. Rokicki, Representing and modeling digital circuits, Ph.D. Thesis, Department of Computer Science, Stanford University, Stanford, CA, USA, 1993. Bengtsson, 2003, On clock difference constraints and termination in reachability analysis of timed automata, vol. 2885 Bouyer, 2004, Forward analysis of updatable timed automata, Formal Methods in System Design, 24, 281, 10.1023/B:FORM.0000026093.21513.31 Bouyer, 2005, Diagonal constraints in timed automata: forward analysis of timed systems, vol. 3829, 112 Reynier, 2007 Asarin, 2002, Timed regular expressions, Journal of the ACM, 49, 172, 10.1145/506147.506151 Bouyer, 2002, A Kleene/Büchi-like theorem for clock languages, Journal of Automata, Languages and Combinatorics, 7, 167 Dima, 2003, Regular expressions with timed dominoes, 141 Dima, 2005, 95 Finkel, 2006, On the shuffle of timed regular languages, Bulletin of the European Association for Theoretical Computer Science, 88, 182 Alur, 2004, Decision problems for timed automata: a survey, vol. 3185, 1 Courcoubetis, 1992, Minimum and maximum delay problems in real-time systems, Formal Methods in System Design, 1, 385, 10.1007/BF00709157 P. Niebert, S. Tripakis, S. Yovine, Minimum-time reachability for timed automata, in: Proceedings of the 8th Mediteranean Conference on Control and Automation, MED2000. Alur, 1994, The observational power of clocks, 162, 10.1007/BFb0015008 Cerans, 1993, Decidability of bisimulation equivalences for parallel timer processes, 302 Larsen, 1997, Time-abstracted bisimulation: implicit specifications and decidability, Information and Computation, 134, 75, 10.1006/inco.1997.2623 Tasiran, 1996, Verifying abstractions of timed systems, 546 Finkel, 2006, Undecidable problems about timed automata, 187 Tripakis, 2006, Folk theorems on the determinization and minimization of timed automata, Information Processing Letters, 99, 222, 10.1016/j.ipl.2006.04.015 Comon, 1999, Timed automata and the theory of real numbers, 242 Alur, 1999, Event-clock automata: a determinizable class of timed automata, Theoretical Computer Science, 211, 253, 10.1016/S0304-3975(97)00173-4 Alur, 2001, Optimal paths in weighted timed automata, 49 Behrmann, 2005, Optimal scheduling using priced timed automata, ACM SIGMETRICS — Performance Evaluation Review, 32, 34, 10.1145/1059816.1059823 Fersman, 2007, Task automata: schedulability, decidability and undecidability, International Journal of Information and Computation, 205, 1149, 10.1016/j.ic.2007.01.009 Behrmann, 2001, Minimum-cost reachability for priced timed automata, 147 Beauquier, 2003, On probabilistic timed automata, Theoretical Computer Science, 292, 65, 10.1016/S0304-3975(01)00215-8 Kwiatkowska, 2002, Automatic verification of real-time systems with discrete probability distributions, Theoretical Computer Science, 282, 101, 10.1016/S0304-3975(01)00046-9 Dang, 2003, Pushdown timed automata: a binary reachability characterization and safety verification, Theoretical Computer Science, 302, 93, 10.1016/S0304-3975(02)00743-0 Bouyer, 2004, Updatable timed automata, Theoretical Computer Science, 321, 291, 10.1016/j.tcs.2004.04.003 Baier, 2007, Probabilistic and topological semantics for timed automata, 179 M. De Wulf, From Timed Models to Timed Implementations. Thèse de doctorat, Département d’Informatique, Université Libre de Bruxelles, Belgium, December 2006. Choffrut, 2000, Timed automata with periodic clock constraints, Journal of Automata, Languages and Combinatorics, 5, 371 Bérard, 2000, Timed automata and additive clock constraints, Information Processing Letters, 75, 1, 10.1016/S0020-0190(00)00075-2 Miller, 2000, Decidability and complexity results for timed automata and semi-linear hybrid automata, 296 Alur, 1993, Parametric real-time reasoning, 592 Hune, 2001, Linear parametric model checking of timed automata, 189 McManis, 1994, Suspension automata: a decidable class of hybrid automata, 105 P.V. Suman, P.K. Pandya, S.N. Krishna, L. Manasa, Timed automata with integer resets: Language inclusion and expressiveness, in: Proceedings of the 6th International Conference on Formal Modeling and Analysis of timed Systems, 2008, pp. 78–92. Manasa, 2011, Model checking weighted integer reset timed automata, Theory of Computing Systems, 48, 648, 10.1007/s00224-010-9253-z Alur, 1993, Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, 209 Henzinger, 1995, What’s decidable about hybrid automata?, 373 Demichelis, 1998, Controlled timed automata, 455 Cassez, 2000, The impressive power of stopwatches, 138 Dima, 2007, Distributed time-asynchronous automata, 185 Akshay, 2008, Distributed timed automata with independently evolving clocks, 82 Bérard, 2009, Interrupt timed automata, 197 Gupta, 1997, Robust timed automata, 331 R. Alur, S.L. Torre, P. Madhusudan, Perturbed timed automata, in: Hybrid Systems, 2005, pp. 70–85. Behrmann, 2001, Efficient guiding towards cost-optimality in UPPAAL, 174 Larsen, 2008, Optimal reachability for multi-priced timed automata, Theoretical Computer Science, 390, 197, 10.1016/j.tcs.2007.09.021 Berendsen, 2006, Probably on time and within budget: On reachability in priced probabilistic timed automata, 311 Norström, 1999, Timed automata as task models for event-driven systems, 182 Jurdziński, 2008, Concavely-priced timed automata, 48 Jurdziński, 2009, Concavely-priced probabilistic timed automata, 415 Barbuti, 2009, Timed P automata, Electronic Notes Theoretical Computer Science, 227, 21, 10.1016/j.entcs.2008.12.102 Bouyer, 2004, Optimal Strategies in Priced Timed Game Automata, vol. 3328, 148 Alur, 1991, Model-checking for probabilistic real-time systems (extended abstract), 115 Kwiatkowska, 2000, Verifying quantitative properties of continuous probabilistic timed automata, 123 Fietzke, 2010, Superposition-based analysis of first-order probabilistic timed automata, 302 P. Krcál, W. Yi, Communicating timed automata: The more synchronous, the more difficult to verify, in: Proceedings of the 18th International Conference on Computer Aided Verification, 2006, pp. 249–262. Lanotte, 2006, Modeling long-running transactions with communicating hierarchical timed automata Pietro, 2003, Automatic verification of multi-queue discrete timed automata, 159 Fellah, 2006, Some succinctness properties of ω-DTAFA, 97 Wang, 2001, Symbolic verification of complex real-time systems with clock-restriction diagram, 235 Ibarra, 2003, Verification in loosely synchronous queue-connected discrete timed automata, Theoretical Computer Science, 290, 1713, 10.1016/S0304-3975(02)00076-2 J. Hoenicke, Combination of processes, data, and time, Ph.D. Thesis, University of Oldenburg, July 2006. Lanotte, 2000, Timed cooperating automata, Fundamenta Informaticae, 43, 153, 10.3233/FI-2000-43123408 D. Beyer, H. Rust, Cottbus timed automata: formal definition and semantics, in: Proceedings of the 2nd IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems, 2001, pp. 75–87. D. D’Souza, M.R. Mohan, Eventual timed automata, in: Proceedings of the 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 2005, pp. 322–334. Henzinger, 1998, The regular real-time languages, 580 D’Souza, 1999, Product interval automata: a subclass of timed automata, 60 D. D’Souza, N. Tabareau, On timed automata with input-determined guards, in: Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems (FORMATS 2004) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 2004), 2004, pp. 68–83. Chevalier, 2006, On continuous timed automata with input-determined guards, 369 Chevalier, 2007, Counter-free input-determined timed automata, 82 Tang, 2009, Event-clock visibly pushdown automata, 558 Dang, 2004, Past pushdown timed automata and safety verification, Theoretical Computer Science, 313, 57, 10.1016/j.tcs.2003.10.004 M. Emmi, R. Majumdar, Decision problems for the verification of real-time software, in: Proceedings of the 9th International Conference on Hybrid Systems: Computation and Control, pp. 200–211, 2006. Trivedi, 2010, Recursive timed automata, 306 M. Benerecetti, S. Minopoli, A. Peron, Analysis of timed recursive state machines, in: Proceedings of the 17th International Symposium on Temporal Representation and Reasoning, 2010, pp. 61–68. Bornot, 1998, Modeling urgency in timed systems, 103 Lin, 2005, Model checking prioritized timed automata, 370 O.N. Timo, A. Rollet, Conformance testing of variable driven automata, in: Proceedings of the 8th IEEE International Workshop on Factory Communication Systems Communication in Automation, 2010. Barbuti, 2004, Timed automata with urgent transitions, Acta Informatica, 40, 317, 10.1007/s00236-003-0135-6 Lasota, 2008, Alternating timed automata, ACM Transactions on Computational Logic, 9, 10.1145/1342991.1342994 Parys, 2009, Weak alternating timed automata, 273 O. Maler, A. Pnueli, J. Sifakis, On the synthesis of discrete controllers for timed systems (an extended abstract), in: Symposium on Theoretical Aspects of Computer Science, pp. 229–242, 1995. Bérard, 1996, On the power of non-observable actions in timed automata, 257 Diekert, 1997, Removing epsilon-transitions in timed automata, 583 Dima, 2009, Removing all silent transitions from timed automata, 118 Lamport, 1987, A fast mutual exclusion algorithm, ACM Transactions on Computer Systems, 5, 1, 10.1145/7351.7352 IEEE Standard for a High-Performance Serial Bus. IEEE Std 1394–1995, 1996. Bozzelli, 2009, Decision problems for lower/upper bound parametric timed automata, Formal Methods in System Design, 35, 121, 10.1007/s10703-009-0074-0 Alur, 2001, Parametric temporal logic for “model measuring”, ACM Transactions on Computational Logic, 2, 388, 10.1145/377978.377990 Bruyère, 2007, Real-time model-checking: Parameters everywhere, Logical Methods in Computer Science, 3, 10.2168/LMCS-3(1:7)2007 Emerson, 1999, Parametric quantitative temporal reasoning, 336 Wang, 1996, Parametric timing analysis for real-time systems, Information and Computation, 130, 131, 10.1006/inco.1996.0086 Zhang, 2005, Fast on-the-fly parametric real-time model checking, 157 É André, IMITATOR II: A tool for solving the good parameters problem in timed automata, in: Proceedings 12th International Workshop on Verification of Infinite-State Systems, 2010, pp. 91–99. Henzinger, 1997, HyTech: a model checker for hybrid systems, 460 Wang, 2006, REDLIB for the formal verification of embedded systems, 341 Wang, 2004, Efficient verification of timed automata with BDD-like data structures, International Journal on Software Tools for Technology Transfer, 6, 77, 10.1007/s10009-003-0135-4 Knapik, 2010, Parametric model checking with VerICS, Transactions on Petri Nets and Other Models of Concurrency, 4, 98, 10.1007/978-3-642-18222-8_5 Annichini, 2001, TReX: a tool for reachability analysis of complex systems, 368 Bouyer, 2005, On conciseness of extensions of timed automata, Journal of Automata, Languages and Combinatorics, 10, 393 Suman, 2009, Determinization and expressiveness of integer reset timed automata with silent transitions, 728 Henzinger, 1996, State equivalences for rectangular hybrid automata, 530 Ghosh, 2004, Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modelling: delta-notch protein signalling, Systems Biology, 1, 170, 10.1049/sb:20045019 Fränzle, 2001, What will be eventually true of polynomial hybrid automata?, 340 Carloni, 2006, Languages and tools for hybrid systems design, Foundations and Trends in Electronic Design Automation, 1, 1, 10.1561/1000000001 Davoren, 2000, Logics for hybrid systems, Proceedings of the IEEE, 88, 985, 10.1109/5.871305 Henzinger, 1996, The theory of hybrid automata, 278 Labinaz, 1997, A survey of modeling and control of hybrid systems, Annual Reviews in Control, 21, 79, 10.1016/S1367-5788(97)00019-9 Tomlin, 2003, Computational techniques for the verification of hybrid systems, Proceedings of the IEEE, 91, 986, 10.1109/JPROC.2003.814621 Tripakis, 2009, Model-based Design of Heterogeneous Systems Bouyer, 2007, On the optimal reachability problem of weighted timed automata, Formal Methods in System Design, 31, 135, 10.1007/s10703-007-0035-4 Behrmann, 2005, Priced timed automata: algorithms and applications, 162 Larsen, 2009, Priced timed automata: theory and tools, vol. 4, 417 Seceleanu, 2009, REMES: a resource model for embedded systems, 84 Ivanov, 2010, REMES tool-chain: a set of integrated tools for behavioral modeling and analysis of embedded systems, 361 T. Brihaye, V. Bruyère, J.-F. Raskin, Model-checking for weighted timed automata, in: Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems (FORMATS 2004) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 2004), pp. 277–292, 2004. Bouyer, 2007, Model-checking one-clock priced timed automata, 108 Bouyer, 2007, Costs are expensive!, vol. 4763, 53 J. Berendsen, D.N. Jansen, F.W. Vaandrager, Fortuna: model checking priced probabilistic timed automata, in: Proceedings of the 7th International Conference on the Quantitative Evaluation of Systems, pp. 273–281, 2010. Bouyer, 2011, Quantitative analysis of real-time systems using priced timed automata, Communications of the ACM, 54, 78, 10.1145/1995376.1995396 Krčál, 2004, Decidable and undecidable problems in schedulability analysis using timed automata, vol. 2988, 236 Amnell, 2002, TIMES — a tool for modelling and implementation of embedded systems, 460 W. Yi, A Calculus of Real Time Systems. Ph.D. thesis, Department of Computer Science, Chalmers University of Technology, 1991. Krčál, 2007, Multi-processor schedulability analysis of preemptive real-time tasks with variable execution times, 274 Păun, 2000, Computing with membranes, Journal of Computer and System Sciences, 61, 108, 10.1006/jcss.1999.1693 Cavaliere, 2005, Time-independent P systems, 239 Jensen, 1996, Model checking probabilistic real time systems, 247 M. Kwiatkowska, G. Norman, R. Segala, J. Sproston, Verifying soft deadlines with probabilistic timed automata, in: Proceedings of the Workshop on Advances in Verification (WAVe 2000), July 2000. Kwiatkowska, 2007, Symbolic model checking for probabilistic timed automata, Information and Computation, 205, 1027, 10.1016/j.ic.2007.01.004 Kwiatkowska, 2011, PRISM 4.0: verification of probabilistic real-time systems mcpta. URL http://www.modestchecker.net/. Shaw, 1992, Communicating real-time state machines, IEEE Transactions on Software Engineering, 18, 805, 10.1109/32.159840 E. Posse, J. Dingel, Theory and implementation of a real-time extension to the π-calculus, in: Proceedings of the 12th IFIP WG 6.1 International Conference and 30th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems, pp. 125–139, 2010. Harel, 1987, Statecharts: a visual formalism for complex systems, Science of Computer Programming, 8, 231, 10.1016/0167-6423(87)90035-9 Booch, 2007 Alur, 1999, Communicating hierarchical state machines, 169 Lanotte, 2008, Design and verification of long-running transactions in a timed framework, Science of Computer Programming, 73, 76, 10.1016/j.scico.2008.07.001 D. Beyer, C. Lewerentz, A. Noack, Rabbit: a tool for BDD-based verification of real-time systems, in: Proceedings of the 15th International Conference on Computer Aided Verification, pp. 122–125, 2003. Lanotte, 2001, Transformations of timed cooperating automata, Fundamenta Informaticae, 47, 271 Drusinsky, 1994, On the power of bounded concurrency I: finite automata, Journal of the ACM, 41, 517, 10.1145/176584.176587 Dima, 1999, Kleene theorems for event-clock automata, 215 D’Souza, 2000, A logical characterisation of event recording automata, 240 D’Souza, 2003, A logical characterisation of event clock automata, International Journal Foundations Computer Science, 14, 625, 10.1142/S0129054103001923 M. Sorea, Tempo: a model-checker for event-recording automata, in: Proceedings of the 1st Workshop on Real-Time Tools, Aalborg, Denmark, August 2001. Penczek, 2001, Towards bounded model checking for Timed Automata, 195 Alur, 2004, Visibly pushdown languages, 202 Chandra, 1981, Alternation, Journal of the ACM, 28, 114, 10.1145/322234.322243 Dickhöfer, 1999, Timed alternating tree automata: the automata-theoretic solution to the TCTL model checking problem, 281 Ouaknine, 2007, On the decidability and complexity of metric temporal logic over finite words, Logical Methods in Computer Science, 3, 10.2168/LMCS-3(1:8)2007 Jenkins, 2010, Alternating timed automata over bounded time, 60 Jones, 1977, Complexity of some problems in Petri nets, Theoretical Computer Science, 4, 277, 10.1016/0304-3975(77)90014-7 Gebremichael, 2005, Specifying urgency in timed I/O automata, 64 Behrmann, 2007, UPPAAL-Tiga: time for playing games!, 121 T. Brihaye, T.A. Henzinger, V.S. Prabhu, J. françois Raskin, Minimum-time reachability in timed games, in: Proceedings of the 34th International Colloquium on Automata, Languages and Programming, pp. 825–837, 2007. Henzinger, 1999, Discrete-time control for rectangular hybrid automata, Theoretical Computer Science, 221, 369, 10.1016/S0304-3975(99)00038-9 M. Jurdzinski, A. Trivedi, Reachability-time games on timed automata, in: Proceedings of the 34th International Colloquium on Automata, Languages and Programming, pp. 838–849, 2007. R. Ehlers, R. Mattmüller, H.-J. Peter, Synthia: verification and synthesis for timed automata, in: Proceedings of the 23rd International Conference on Computer Aided Verification, Cliff Lodge, Snowbird, Utah, USA, July 2011. F. Cassez, N. Markey, Communicating Embedded Systems–Software and Design, Control of Timed Systems, pp. 83–120. 2009 (Chapter). Cassez, 2002, A comparison of control problems for timed and hybrid systems, 134 Daws, 2006, Symbolic robustness analysis of timed automata, vol. 4202, 143 Swaminathan, 2007, A symbolic decision procedure for robust safety of timed systems, 192 Dima, 2007, Dynamical properties of timed automata revisited, 130 Bouyer, 2006, Robust model-checking of linear-time properties in timed automata, vol. 3887, 238 R. Jaubert, P.-A. Reynier, Quantitative robustness analysis of flat timed automata, in: Proceedings of the 14th International Conference on Foundations of Software Science and Computational Structures: Part of the joint European Conferences on Theory and Practice of Software, pp. 229–244, 2011. Larsen, 2011, Robust specification of real time components, 129 Ouaknine, 2003, Revisiting digitization, robustness, and decidability for timed automata, 198 M. Swaminathan, M. Fränzle, J.-P. Katoen, The surprising robustness of (closed) timed automata against clock-drift, in: Proceedings of the 5th IFIP International Conference on Theoretical Computer Science, pp. 537–553, 2008. K. Altisen, S. Tripakis, Implementation of timed automata: an issue of semantics or modeling?, in: Proceedings of the 3rd International Conference on Formal Modeling and Analysis of Timed Systems, pp. 273–288, 2005. Abdulla, 2010, Sampled semantics of timed automata, Logical Methods in Computer Science, 6 Bouyer, 2011, Timed automata can always be made implementable, vol. 6901 Asarin, 1998, On discretization of delays in timed automata and digital circuits, 470 Krčál, 2005, On sampled semantics of timed systems, vol. 3821, 310 Bosscher, 1994, Verification of an audio control protocol, 170 Wellings, 2004 N. Hakimipour, P.A. Strooper, R. Duke, Exploring model-based development for the verification of real-time Java code, in: Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, 2008. Hakimipour, 2010, TART: Timed-automata to real-time java tool, 299 Jee, 2010, A safety-assured development approach for real-time software, 133 P. Kuc˘era, O. Hync˘ica, P. Honzík, Implementation of timed automata in a real-time operating system, in: Proceedings of World Congress on Engineering and Computer Science, vol. I, pp. 56–60, October 2010. Ouimet, 2007, The TASM toolset: specification, simulation, and formal verification of real-time systems, 126 Campana, 2008, XAL: a web oriented programming language based on timed-automata, 862 Lv, 2011, McAiT: a timing analyzer for multicore real-time software, 414 UPPAAL PRO. URL http://www.cs.aau.dk/~arild/uppaal-probabilistic/. Håkansson, 2008, Component-based design and analysis of embedded systems with UPPAAL PORT, 252 A. Hessel, P. Pettersson, CoVer — a real-time test case generation tool, in: Proceedings of the 19th IFIP International Conference on Testing of Communicating Systems and 7th International Workshop on Formal Approaches to Testing of Software, 2007. Larsen, 2005, Testing real-time embedded software using UPPAAL-TRON: an industrial case study, 299 P. Krčál, L. Mokrushin, W. Yi, A tool for compositional analysis of timed systems by abstraction (extended abstract), in: E. B. Johnsen, O. Owe, and G. Schneider, (Eds.), Proceedings of the 19th Nordic Workshop on Programming Theory, 2007. Sentilles, 2009, Save-IDE — a tool for design, analysis and implementation of component-based embedded systems, 607 K. Altisen, S. Tripakis, Tools for controller synthesis of timed systems, in: Proceedings of the 2nd Workshop on Real-Time Tools, July 2002. Closse, 2001, TAXYS: a tool for the development and verification of real-time embedded systems, 391 Tripakis, 1996, Extending Promela and Spin for real time, 329 M. Bozga, S. Graf, I. Ober, I. Ober, J. Sifakis, The IF toolset, in: Proceedings of the 4th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time, in: LNCS, vol. 3185, June 2004. Laroussinie, 1998, CMC: a tool for compositional model-checking of real-time systems, 439 Kupferschmid, 2008, Faster than UPPAAL?, 552 Didier, 2009, The mirela framework: modeling and analyzing mixed reality applications using timed automata, Journal of Virtual Reality and Broadcasting, 6 Cambronero, 2011, Validation and verification of web services choreographies by using timed automata, Journal of Logic and Algebraic Programming, 80, 25, 10.1016/j.jlap.2010.02.001 Bendiksen, 2009, The priced-timed maude tool, 443 Madl, 2006 A. Alfonso, V. Braberman, D. Garbervetsky, N. Kicillof, A. Olivero, F. Schapachnik, VInTiMe: combining high-level finesse with low-level muscle to verify real-time systems, in: Proceedings of the 1st International Conference on Principles of Software Engineering, Buenos Aires, Argentina, October, 2004. Braberman, 1999, Verification of real-time designs: Combining scheduling theory with automatic formal verification, 494 Alfonso, 2004, Visual timed event scenarios, 168 Braberman, 2004, ObsSlice: a timed automata slicer based on observers, vol. 3114, 470 Braberman, 2005, Issues in distributed timed model checking: Building Zeus, International Journal on Software Tools for Technology Transfer, 7, 4, 10.1007/s10009-004-0143-z Larsen, 1999, Clock difference diagrams, Nordic Journal of Computing, 6, 271 Asarin, 1997, Data-structures for the verification of timed automata, vol. 1201, 346 T. Wilke, Automaten und Logiken für zeitabhngige Systeme. Dissertation, Christian-Albrechts-Universität zu Kiel, 1994.