×

zbMATH — the first resource for mathematics

A survey of timed automata for the development of real-time systems. (English) Zbl 1302.68180
Summary: Timed automata are a popular formalism to model real-time systems. They were introduced two decades ago to support formal verification. Since then they have also been used for other purposes and a large number of variants has been introduced to be able to deal with the many different kinds of requirements of real-time system development. This survey attempts to introduce a massive and complicated theoretical research area to a reader in an easy and compact manner. One objective of this paper is to inform a reader about the theoretical properties (or capabilities) of timed automata which are (or might be) useful for real-time model driven development. To achieve this goal, this paper presents a survey on semantics, decision problems, and variants of timed automata. The other objective of this paper is to inform a reader about the current state of the art of timed automata in practice. To achieve the second aim, this article presents a survey on timed automata’s implementability and tools.

MSC:
68Q45 Formal languages and automata
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
68-02 Research exposition (monographs, survey articles) pertaining to computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R.; Dill, D. L., Automata for modeling real-time systems, (Proceedings of the 17th International Colloquium on Automata, Languages and Programming, (1990), Springer-Verlag New York, Inc New York, NY, USA), 322-335 · Zbl 0765.68150
[2] Alur, R.; Dill, D. L., A theory of timed automata, Theoretical Computer Science, 126, 183-235, (1994) · Zbl 0803.68071
[3] Henzinger, T. A.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Information and Computation, 111, 394-406, (1994)
[4] Alur, R., Timed automata, Theoretical Computer Science, 126, 183-235, (1999) · Zbl 0803.68071
[5] Bérard, B.; Petit, A.; Diekert, V.; Gastin, P., Characterization of the expressive power of silent transitions in timed automata, Fundamenta Informaticae, 36, 145-182, (1998) · Zbl 0930.68077
[6] Alur, R.; Courcoubetis, C.; Dill, D., Model-checking in dense real-time, Information and Computation, 104, 2-34, (1993) · Zbl 0783.68076
[7] Fersman, E.; Pettersson, P.; Yi, W., Timed automata with asynchronous processes: schedulability and decidability, (Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’02, (2002), Springer-Verlag London, UK), 67-82 · Zbl 1043.68589
[8] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Dill, D. L.; Wong-Toi, H., Minimization of timed transition systems, (Proceedings of the 3rd International Conference on Concurrency Theory, CONCUR’92, (1992), Springer-Verlag London, UK), 340-354
[9] Tripakis, S.; Yovine, S., Analysis of timed systems using time-abstracting bisimulations, Formal Methods in System Design, 18, 25-68, (2001) · Zbl 0971.68096
[10] Dill, D. L., Timing assumptions and verification of finite-state concurrent systems, (Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, (1990), Springer-Verlag New York, Inc New York, NY, USA), 197-212
[11] Puri, A., Dynamical properties of timed automata, (Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT’98, (1998), Springer-Verlag London, UK), 210-227
[12] M. Sorea, Verification of real-time systems through lazy approximations, Ph.D. Thesis, Universität Ulm, Germany, 2003.
[13] Behrmann, G.; David, A.; Larsen, K. G.; Pettersson, P.; Yi, W., Developing UPPAAL over 15 years, Software: Practice and Experience, 41, 2, 133-142, (2011), ISSN 0038-0644
[14] Daws, C.; Olivero, A.; Tripakis, S.; Yovine, S., The tool KRONOS, (Proceedings of the DIMACS/SYCON Workshop on Hybrid Systems III: Verification and Control, (1996), Springer-Verlag New York, Inc Secaucus, NJ, USA), 208-219
[15] Bellman, R., Dynamic programming, (1957), Princeton University Press · Zbl 0077.13605
[16] J. Bengtsson, Clocks, DBMs and states in timed systems. Ph.D. Thesis, Department of Information Technology, Uppsala University, Uppsala, Sweden, 2002.
[17] Bengtsson, J.; Yi, W., Timed automata: semantics, algorithms and tools, (Reisig, W.; Rozenberg, G., Lecture Notes on Concurrency and Petri Nets, Lecture Notes in Computer Science, vol. 3098, (2004), Springer-Verlag) · Zbl 1088.68119
[18] Daws, C.; Tripakis, S., Model checking of real-time reachability properties using abstractions, (Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, (1998), Springer-Verlag London, UK), 313-329
[19] Bouajjani, A.; Tripakis, S.; Yovine, S., On-the-fly symbolic model checking for real-time systems, (Proceedings of the 18th IEEE Real-Time Systems Symposium, RTSS’97, (1997), IEEE Computer Society Washington, DC, USA), 232-243
[20] Tripakis, S.; Yovine, S.; Bouajjani, A., Checking timed Büchi automata emptiness efficiently, Formal Methods in System Design, 26, 267-292, (2005) · Zbl 1085.68083
[21] Tripakis, S., Checking timed Büchi automata emptiness on simulation graphs, ACM Transactions on Computational Logic, 10, (2009), 15: 1-15: 19 · Zbl 1352.68165
[22] T.G. Rokicki, Representing and modeling digital circuits, Ph.D. Thesis, Department of Computer Science, Stanford University, Stanford, CA, USA, 1993.
[23] Bengtsson, J.; Yi, W., On clock difference constraints and termination in reachability analysis of timed automata, (Dong, J. S.; Woodcock, J., Proceedings of the 5th International Conference on Formal Engineering Methods, Lecture Notes in Computer Science, vol. 2885, (2003), Springer-Verlag)
[24] Bouyer, P., Forward analysis of updatable timed automata, Formal Methods in System Design, 24, 281-320, (2004), ISSN 0925-9856 · Zbl 1073.68041
[25] Bouyer, P.; Laroussinie, F.; Reynier, P.-A., Diagonal constraints in timed automata: forward analysis of timed systems, (Pettersson, P.; Yi, W., Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS’05, Lecture Notes in Computer Science, vol. 3829, (2005), Springer Uppsala, Sweden), 112-126 · Zbl 1175.68256
[26] Reynier, P.-A., Diagonal constraints handled efficiently in UPPAAL. technical report LSV-07-02, laboratoire spcification et vrification, ENS cachan, France, (2007)
[27] Asarin, E.; Caspi, P.; Maler, O., Timed regular expressions, Journal of the ACM, 49, 2, 172-206, (2002) · Zbl 1323.68335
[28] Bouyer, P.; Petit, A., A Kleene/Büchi-like theorem for clock languages, Journal of Automata, Languages and Combinatorics, 7, 2, 167-186, (2002) · Zbl 1031.68121
[29] Dima, C., Regular expressions with timed dominoes, (Proceedings of the 4th International Conference on Discrete Mathematics and Theoretical Computer Science, DMTCS’03, (2003), Springer-Verlag Berlin, Heidelberg), 141-154 · Zbl 1040.68052
[30] Dima, C., Timed shuffle expressions, 95-109, (2005), Springer-Verlag London, UK · Zbl 1134.68384
[31] Finkel, O., On the shuffle of timed regular languages, Bulletin of the European Association for Theoretical Computer Science, 88, 182-184, (2006) · Zbl 1169.68468
[32] Alur, R.; Madhusudan, P., Decision problems for timed automata: a survey, (Bernardo, M.; Corradini, F., Formal Methods for the Design of Real-Time Systems — Revised Lectures of the International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT’04, Lecture Notes in Computer Science, vol. 3185, (2004), Springer-Verlag), 1-24 · Zbl 1105.68057
[33] Courcoubetis, C.; Yannakakis, M., Minimum and maximum delay problems in real-time systems, Formal Methods in System Design, 1, 385-415, (1992) · Zbl 0777.68045
[34] P. Niebert, S. Tripakis, S. Yovine, Minimum-time reachability for timed automata, in: Proceedings of the 8th Mediteranean Conference on Control and Automation, MED2000.
[35] Alur, R.; Courcoubetis, C.; Henzinger, T. A., The observational power of clocks, (Lecture Notes in Computer Science, vol. 836, (1994), Springer-Verlag), 162-177
[36] Cerans, K., Decidability of bisimulation equivalences for parallel timer processes, (Proceedings of the 4th International Workshop on Computer Aided Verification, (1993), Springer-Verlag London, UK), 302-315
[37] Larsen, K. G.; Wang, Y., Time-abstracted bisimulation: implicit specifications and decidability, Information and Computation, 134, 75-101, (1997) · Zbl 0887.68068
[38] Tasiran, S.; Alur, R.; Kurshan, R. P.; Brayton, R. K., Verifying abstractions of timed systems, (Proceedings of the 7th International Conference on Concurrency Theory, CONCUR’96, (1996), Springer-Verlag London, UK), 546-562
[39] Finkel, O., Undecidable problems about timed automata, (Proceedings of the 4th international conference on Formal Modeling and Analysis of Timed Systems, FORMATS’06, (2006), Springer-Verlag Berlin, Heidelberg), 187-199 · Zbl 1141.68433
[40] Tripakis, S., Folk theorems on the determinization and minimization of timed automata, Information Processing Letters, 99, 6, 222-226, (2006) · Zbl 1185.68401
[41] Comon, H.; Jurski, Y., Timed automata and the theory of real numbers, (Proceedings of the 10th International Conference on Concurrency Theory, CONCUR’99, (1999), Springer-Verlag London, UK), 242-257 · Zbl 0940.68092
[42] Alur, R.; Fix, L.; Henzinger, T. A., Event-clock automata: a determinizable class of timed automata, Theoretical Computer Science, 211, 253-273, (1999) · Zbl 0912.68132
[43] Alur, R.; Torre, S. L.; Pappas, G. J., Optimal paths in weighted timed automata, (Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control, HSCC’01, (2001), Springer-Verlag London, UK), 49-62 · Zbl 0991.93076
[44] Behrmann, G.; Larsen, K. G.; Rasmussen, J. I., Optimal scheduling using priced timed automata, ACM SIGMETRICS — Performance Evaluation Review, 32, 34-40, (2005)
[45] Fersman, E.; Krčál, P.; Pettersson, P.; Yi, W., Task automata: schedulability, decidability and undecidability, International Journal of Information and Computation, 205, 1149-1172, (2007) · Zbl 1121.68062
[46] Behrmann, G.; Fehnker, A.; Hune, T.; Larsen, K. G.; Pettersson, P.; Romijn, J.; Vaandrager, F. W., Minimum-cost reachability for priced timed automata, (Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control, HSCC’01, (2001), Springer-Verlag London, UK), 147-161 · Zbl 0991.68037
[47] Beauquier, D., On probabilistic timed automata, Theoretical Computer Science, 292, 65-84, (2003) · Zbl 1064.68063
[48] Kwiatkowska, M.; Norman, G.; Segala, R.; Sproston, J., Automatic verification of real-time systems with discrete probability distributions, Theoretical Computer Science, 282, 101-150, (2002) · Zbl 1050.68094
[49] Dang, Z., Pushdown timed automata: a binary reachability characterization and safety verification, Theoretical Computer Science, 302, 93-121, (2003) · Zbl 1044.68085
[50] Bouyer, P.; Dufourd, C.; Fleury, E.; Petit, A., Updatable timed automata, Theoretical Computer Science, 321, 291-345, (2004) · Zbl 1070.68063
[51] Baier, C.; Bertrand, N.; Bouyer, P.; Brihaye, T.; Größer, M., Probabilistic and topological semantics for timed automata, (Proceedings of the 27th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’07, (2007), Springer-Verlag Berlin, Heidelberg), 179-191 · Zbl 1135.68464
[52] M. De Wulf, From Timed Models to Timed Implementations. Thèse de doctorat, Département d’Informatique, Université Libre de Bruxelles, Belgium, December 2006.
[53] Choffrut, C.; Goldwurm, M., Timed automata with periodic clock constraints, Journal of Automata, Languages and Combinatorics, 5, 371-403, (2000) · Zbl 0964.68076
[54] Bérard, B.; Dufourd, C., Timed automata and additive clock constraints, Information Processing Letters, 75, 1-7, (2000) · Zbl 0953.68565
[55] Miller, J. S., Decidability and complexity results for timed automata and semi-linear hybrid automata, (Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control, HSCC’00, (2000), Springer-Verlag London, UK), 296-309 · Zbl 0992.93050
[56] Alur, R.; Henzinger, T. A.; Vardi, M. Y., Parametric real-time reasoning, (Proceedings of the 25th Annual ACM Symposium on Theory of Computing, STOC’93, (1993), ACM New York, NY, USA), 592-601 · Zbl 1310.68139
[57] Hune, T.; Romijn, J.; Stoelinga, M.; Vaandrager, F. W., Linear parametric model checking of timed automata, (Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, (2001), Springer-Verlag London, UK), 189-203 · Zbl 0978.68094
[58] McManis, J.; Varaiya, P., Suspension automata: a decidable class of hybrid automata, (Proceedings of the 6th International Conference on Computer Aided Verification, CAV’94, (1994), Springer-Verlag London, UK), 105-117
[59] 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. · Zbl 1171.68536
[60] Manasa, L.; Krishna, S. N.; Jain, C., Model checking weighted integer reset timed automata, Theory of Computing Systems, 48, 3, 648-679, (2011) · Zbl 1217.68139
[61] Alur, R.; Courcoubetis, C.; Henzinger, T. A.; Ho, P.-H., Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, (Hybrid Systems, (1993), Springer-Verlag London, UK), 209-229
[62] Henzinger, T. A.; Kopke, P. W.; Puri, A.; Varaiya, P., What’s decidable about hybrid automata?, (Proceedings of the 27th Annual ACM Symposium on Theory of Computing, STOC’95, (1995), ACM New York, NY, USA), 373-382 · Zbl 0978.68534
[63] Demichelis, F.; Zielonka, W., Controlled timed automata, (Proceedings of the 9th International Conference on Concurrency Theory, CONCUR’98, (1998), Springer-Verlag London, UK), 455-469
[64] Cassez, F.; Larsen, K. G., The impressive power of stopwatches, (Proceedings of the 11th International Conference on Concurrency Theory, CONCUR’00, (2000), Springer-Verlag London, UK), 138-152 · Zbl 0999.68112
[65] Dima, C.; Lanotte, R., Distributed time-asynchronous automata, (Proceedings of the 4th International Conference on Theoretical Aspects of Computing, ICTAC’07, (2007), Springer-Verlag Berlin, Heidelberg), 185-200 · Zbl 1147.68556
[66] Akshay, S.; Bollig, B.; Gastin, P.; Mukund, M.; Narayan Kumar, K., Distributed timed automata with independently evolving clocks, (Proceedings of the 19th International Conference on Concurrency Theory, CONCUR’08, (2008), Springer-Verlag Berlin, Heidelberg), 82-97 · Zbl 1160.68450
[67] Bérard, B.; Haddad, S., Interrupt timed automata, (Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, FOSSACS’09, (2009), Springer-Verlag Berlin, Heidelberg), 197-211 · Zbl 1234.68195
[68] Gupta, V.; Henzinger, T. A.; Jagadeesan, R., Robust timed automata, (Proceedings of the International Workshop on Hybrid and Real-Time Systems, (1997), Springer-Verlag London, UK), 331-345
[69] R. Alur, S.L. Torre, P. Madhusudan, Perturbed timed automata, in: Hybrid Systems, 2005, pp. 70-85.
[70] Behrmann, G.; Fehnker, A.; Hune, T.; Larsen, K. G.; Pettersson, P.; Romijn, J., Efficient guiding towards cost-optimality in UPPAAL, (Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, (2001), Springer-Verlag London, UK), 174-188 · Zbl 0978.68541
[71] Larsen, K. G.; Rasmussen, J. I., Optimal reachability for multi-priced timed automata, Theoretical Computer Science, 390, 197-213, (2008) · Zbl 1134.68029
[72] Berendsen, J.; Jansen, D. N.; Katoen, J.-P., Probably on time and within budget: on reachability in priced probabilistic timed automata, (Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems, (2006), IEEE Computer Society Washington, DC, USA), 311-322
[73] Norström, C.; Wall, A.; Yi, W., Timed automata as task models for event-driven systems, (Proceedings of the 6th International Conference on Real-Time Computing Systems and Applications, RTCSA’99, (1999), IEEE Computer Society Washington, DC, USA), 182-189
[74] Jurdziński, M.; Trivedi, A., Concavely-priced timed automata, (Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS’08, (2008), Springer-Verlag Berlin, Heidelberg), 48-62 · Zbl 1171.68529
[75] Jurdziński, M.; Kwiatkowska, M.; Norman, G.; Trivedi, A., Concavely-priced probabilistic timed automata, (Proceedings of the 20th International Conference on Concurrency Theory, CONCUR 2009, (2009), Springer-Verlag Berlin, Heidelberg), 415-430 · Zbl 1254.68136
[76] Barbuti, R.; Maggiolo-Schettini, A.; Milazzo, P.; Tesei, L., Timed P automata, Electronic Notes Theoretical Computer Science, 227, 21-36, (2009) · Zbl 1347.68127
[77] Bouyer, P.; Cassez, F.; Fleury, E.; Larsen, K. G., Optimal strategies in priced timed game automata, (Lodaya, K.; Mahajan, M., Proceedings of the 24th Conference on Fundations of Software Technology and Theoretical Computer Science, FSTTCS’04, Lecture Notes in Computer Science, vol. 3328, (2004), Springer Chennai, India), 148-160 · Zbl 1117.68396
[78] Alur, R.; Courcoubetis, C.; Dill, D., Model-checking for probabilistic real-time systems (extended abstract), (Proceedings of the 18th International Colloquium on Automata, Languages and Programming, (1991), Springer-Verlag New York, Inc New York, NY, USA), 115-126 · Zbl 0769.68088
[79] Kwiatkowska, M. Z.; Norman, G.; Segala, R.; Sproston, J., Verifying quantitative properties of continuous probabilistic timed automata, (Proceedings of the 11th International Conference on Concurrency Theory, CONCUR’00, (2000), Springer-Verlag London, UK), 123-137 · Zbl 0999.68125
[80] Fietzke, A.; Hermanns, H.; Weidenbach, C., Superposition-based analysis of first-order probabilistic timed automata, (Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’10, (2010), Springer-Verlag Berlin, Heidelberg), 302-316 · Zbl 1306.68095
[81] 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. · Zbl 1188.68192
[82] Lanotte, R.; Maggiolo-schettini, A.; Milazzo, P.; Troina, A., Modeling long-running transactions with communicating hierarchical timed automata, (Proceedings of the 8th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, (2006), Springer)
[83] Pietro, P. S.; Dang, Z., Automatic verification of multi-queue discrete timed automata, (Proceedings of the 9th Annual International Conference on Computing and Combinatorics, COCOON’03, (2003), Springer-Verlag Berlin, Heidelberg), 159-171 · Zbl 1276.68097
[84] Fellah, A.; Noureddine, S., Some succinctness properties of \(\omega\)-DTAFA, (Proceedings of the 5th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, (2006), World Scientific and Engineering Academy and Society Stevens Point, Wisconsin, USA), 97-103
[85] Wang, F., Symbolic verification of complex real-time systems with clock-restriction diagram, (Proceedings of the IFIP TC6/WG6.1 — 21st International Conference on Formal Techniques for Networked and Distributed Systems, FORTE’01, (2001), Kluwer, B.V), 235-250
[86] Ibarra, O. H.; Dang, Z.; Pietro, P. S., Verification in loosely synchronous queue-connected discrete timed automata, Theoretical Computer Science, 290, 1713-1735, (2003) · Zbl 1044.68096
[87] J. Hoenicke, Combination of processes, data, and time, Ph.D. Thesis, University of Oldenburg, July 2006.
[88] Lanotte, R.; Maggiolo-Schettini, A.; Peron, A., Timed cooperating automata, Fundamenta Informaticae, 43, 153-173, (2000) · Zbl 0965.68046
[89] 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.
[90] 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. · Zbl 1172.68499
[91] Henzinger, T. A.; Raskin, J.-F.; Schobbens, P.-Y., The regular real-time languages, (Proceedings of the 25th International Colloquium on Automata, Languages, and Programming, ICALP’98, (1998), Springer-Verlag London, UK), 580-591
[92] D’Souza, D.; Thiagarajan, P. S., Product interval automata: a subclass of timed automata, (Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science, (1999), Springer-Verlag London, UK), 60-71 · Zbl 0958.68087
[93] 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.
[94] Chevalier, F.; Deepak D’Souza, D.; Prabhakar, P., On continuous timed automata with input-determined guards, (Proceedings of the 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS’06, (2006), Springer-Verlag Berlin, Heidelberg), 369-380 · Zbl 1177.68136
[95] Chevalier, F.; D’Souza, D.; Prabhakar, P., Counter-free input-determined timed automata, (Proceedings of the 5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS’07, (2007), Springer-Verlag Berlin, Heidelberg), 82-97 · Zbl 1142.68039
[96] Tang, N.; Ogawa, M., Event-clock visibly pushdown automata, (Proceedings of the 35th Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM’09, (2009), Springer-Verlag Berlin, Heidelberg), 558-569 · Zbl 1206.68183
[97] Dang, Z.; Bultan, T.; Ibarra, O. H.; Kemmerer, R. A., Past pushdown timed automata and safety verification, Theoretical Computer Science, 313, 57-71, (2004) · Zbl 1069.68065
[98] 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. · Zbl 1178.68340
[99] Trivedi, A.; Wojtczak, D., Recursive timed automata, (Proceedings of the 8th International Conference on Automated Technology for Verification and Analysis, ATVA’10, (2010), Springer-Verlag Berlin, Heidelberg), 306-324 · Zbl 1305.68115
[100] 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.
[101] Bornot, S.; Sifakis, J.; Tripakis, S., Modeling urgency in timed systems, (Revised Lectures from the International Symposium on Compositionality: The Significant Difference, COMPOS’97, (1998), Springer-Verlag London, UK), 103-129
[102] Lin, S.-W.; Hsiung, P.-A.; Huang, C.-H.; Chen, Y.-R., Model checking prioritized timed automata, (Proceedings of the 3rd International Conference on Automated Technology for Verification and Analysis, ATVA’05, (2005), Springer-Verlag Berlin, Heidelberg), 370-384 · Zbl 1170.68521
[103] 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.
[104] Barbuti, R.; Tesei, L., Timed automata with urgent transitions, Acta Informatica, 40, 317-347, (2004) · Zbl 1072.68053
[105] Lasota, S.; Walukiewicz, I., Alternating timed automata, ACM Transactions on Computational Logic, 9, (2008), 10: 1-10: 27 · Zbl 1367.68172
[106] Parys, P.; Walukiewicz, I., Weak alternating timed automata, (Proceedings of the 36th Internatilonal Colloquium on Automata, Languages and Programming: Part II, ICALP’09, (2009), Springer-Verlag Berlin, Heidelberg), 273-284 · Zbl 1248.03058
[107] 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. · Zbl 1379.68227
[108] Bérard, B.; Gastin, P.; Petit, A., On the power of non-observable actions in timed automata, (Proceedings of the 13th Annual Symposium on Theoretical Aspects of Computer Science, (1996), Springer-Verlag London, UK), 257-268 · Zbl 1379.68216
[109] Diekert, V.; Gastin, P.; Petit, A., Removing epsilon-transitions in timed automata, (Proceedings of the 14th Annual Symposium on Theoretical Aspects of Computer Science, STACS’97, (1997), Springer-Verlag London, UK), 583-594
[110] Dima, C.; Lanotte, R., Removing all silent transitions from timed automata, (Proceedings of the 7th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS’09, (2009), Springer-Verlag Berlin, Heidelberg), 118-132 · Zbl 1262.68089
[111] Lamport, L., A fast mutual exclusion algorithm, ACM Transactions on Computer Systems, 5, 1-11, (1987)
[112] IEEE Standard for a High-Performance Serial Bus. IEEE Std 1394-1995, 1996.
[113] Bozzelli, L.; La Torre, S., Decision problems for lower/upper bound parametric timed automata, Formal Methods in System Design, 35, 121-151, (2009) · Zbl 1186.68245
[114] Alur, R.; Etessami, K.; La Torre, S.; Peled, D., Parametric temporal logic for “model measuring”, ACM Transactions on Computational Logic, 2, 388-407, (2001) · Zbl 1171.68544
[115] Bruyère, V.; Raskin, J.-F., Real-time model-checking: parameters everywhere, Logical Methods in Computer Science, 3, 1, (2007) · Zbl 1128.68052
[116] Emerson, E. A.; Trefler, R. J., Parametric quantitative temporal reasoning, (Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS’99, (1999), IEEE Computer Society Washington, DC, USA), 336-343
[117] Wang, F., Parametric timing analysis for real-time systems, Information and Computation, 130, 131-150, (1996) · Zbl 0872.68041
[118] Zhang, D.; Cleaveland, R., Fast on-the-fly parametric real-time model checking, (Proceedings of the 26th IEEE International Real-Time Systems Symposium, (2005), IEEE Computer Society Washington, DC, USA), 157-166
[119] É 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.
[120] Henzinger, T. A.; Ho, P.-H.; Wong-Toi, H., Hytech: a model checker for hybrid systems, (Proceedings of the 9th International Conference on Computer Aided Verification, CAV ’97, (1997), Springer-Verlag London, UK), 460-463 · Zbl 1060.68603
[121] Wang, F., REDLIB for the formal verification of embedded systems, (Proceedings of the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, (2006), IEEE Computer Society Washington, DC, USA), 341-346
[122] Wang, F., Efficient verification of timed automata with BDD-like data structures, International Journal on Software Tools for Technology Transfer, 6, 77-97, (2004)
[123] Knapik, M.; Niewiadomski, A.; Penczek, W.; Pólrola, A.; Szreter, M.; Zbrzezny, A., Parametric model checking with verics, Transactions on Petri Nets and Other Models of Concurrency, 4, 98-120, (2010) · Zbl 1312.68134
[124] Annichini, A.; Bouajjani, A.; Sighireanu, M., Trex: a tool for reachability analysis of complex systems, (Proceedings of the 13th International Conference on Computer Aided Verification, CAV’01, (2001), Springer-Verlag London, UK), 368-372 · Zbl 0991.68645
[125] Bouyer, P.; Chevalier, F., On conciseness of extensions of timed automata, Journal of Automata, Languages and Combinatorics, 10, 393-405, (2005) · Zbl 1146.68384
[126] Suman, P. V.; Pandya, P. K., Determinization and expressiveness of integer reset timed automata with silent transitions, (Proceedings of the 3rd International Conference on Language and Automata Theory and Applications, LATA’09, (2009), Springer-Verlag Berlin, Heidelberg), 728-739 · Zbl 1234.68242
[127] Henzinger, T. A.; Kopke, P. W., State equivalences for rectangular hybrid automata, (Proceedings of the 7th International Conference on Concurrency Theory, CONCUR’96, (1996), Springer-Verlag London, UK), 530-545
[128] Ghosh, R.; Tomlin, C., Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modelling: delta-notch protein signalling, Systems Biology, 1, 170-183, (2004)
[129] Fränzle, M., What will be eventually true of polynomial hybrid automata?, (Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, TACS’01, (2001), Springer-Verlag London, UK), 340-359 · Zbl 1087.68571
[130] Carloni, L. P.; Passerone, R.; Pinto, A.; Sangiovanni-Vincentelli, A. L., Languages and tools for hybrid systems design, Foundations and Trends in Electronic Design Automation, 1, 1-193, (2006) · Zbl 1107.68385
[131] Davoren, J. M.; Nerode, A., Logics for hybrid systems, Proceedings of the IEEE, 88, 985-1010, (2000)
[132] Henzinger, T. A., The theory of hybrid automata, (Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS’96, (1996), IEEE Computer Society Washington, DC, USA), 278
[133] Labinaz, G.; Bayoumi, M. M.; Rudie, K., A survey of modeling and control of hybrid systems, Annual Reviews in Control, 21, 79-92, (1997)
[134] Tomlin, C.; Mitchell, I.; Bayen, A. M.; Oishi, M., Computational techniques for the verification of hybrid systems, Proceedings of the IEEE, 91, 986-1001, (2003)
[135] Tripakis, S.; Dang, T., Model-based design of heterogeneous systems, (Modeling, Verification and Testing using Timed and Hybrid Automata, (2009), CRC Press), (Chapter)
[136] Bouyer, P.; Brihaye, T.; Bruyère, V.; Raskin, J.-F., On the optimal reachability problem of weighted timed automata, Formal Methods in System Design, 31, 135-175, (2007) · Zbl 1129.68039
[137] Behrmann, G.; Larsen, K. G.; Rasmussen, J. I., Priced timed automata: algorithms and applications, (Proceedings of the 3rd International Conference on Formal Methods for Components and Objects, FMCO’04, (2005), Springer-Verlag Berlin, Heidelberg), 162-182 · Zbl 1143.68430
[138] Larsen, K. G., Priced timed automata: theory and tools, (Kannan, R.; Kumar, K. N., IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2009, Leibniz International Proceedings in Informatics, LIPIcs, vol. 4, (2009), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl, Germany), 417-425 · Zbl 1248.68335
[139] Seceleanu, C.; Vulgarakis, A.; Pettersson, P., REMES: a resource model for embedded systems, (Proceedings of the 14th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS’09, (2009), IEEE Computer Society Washington, DC, USA), 84-94
[140] Ivanov, D.; Orlić, M.; Seceleanu, C.; Vulgarakis, A., REMES tool-chain: a set of integrated tools for behavioral modeling and analysis of embedded systems, (Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, ASE’10, (2010), ACM New York, NY, USA), 361-362
[141] 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. · Zbl 1109.68512
[142] Bouyer, P.; Larsen, K. G.; Markey, N., Model-checking one-clock priced timed automata, (Proceedings of the 10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS’07, (2007), Springer-Verlag Berlin, Heidelberg), 108-122 · Zbl 1149.68400
[143] Bouyer, P.; Markey, N., Costs are expensive!, (Raskin, J.-F.; Thiagarajan, P. S., Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems, FORMATS’07, Lecture Notes in Computer Science, vol. 4763, (2007), Springer Salzburg, Austria), 53-68 · Zbl 1142.68045
[144] 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.
[145] Bouyer, P.; Fahrenberg, U.; Larsen, K. G.; Markey, N., Quantitative analysis of real-time systems using priced timed automata, Communications of the ACM, 54, 78-87, (2011)
[146] Krčál, P.; Yi, W., Decidable and undecidable problems in schedulability analysis using timed automata, (Jensen, K.; Podelski, A., Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, vol. 2988, (2004), Springer-Verlag), 236-250 · Zbl 1126.68456
[147] Amnell, T.; Fersman, E.; Mokrushin, L.; Pettersson, P.; Yi, W., TIMES — a tool for modelling and implementation of embedded systems, (Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’02, (2002), Springer-Verlag London, UK), 460-464 · Zbl 1043.68513
[148] W. Yi, A Calculus of Real Time Systems. Ph.D. thesis, Department of Computer Science, Chalmers University of Technology, 1991.
[149] Krčál, P.; Stigge, M.; Yi, W., Multi-processor schedulability analysis of preemptive real-time tasks with variable execution times, (Proceedings of the 5th International Conference on Formal Modeling and Analysis of timed Systems, FORMATS’07, (2007), Springer-Verlag Berlin, Heidelberg), 274-289 · Zbl 1141.68353
[150] Păun, G., Computing with membranes, Journal of Computer and System Sciences, 61, 108-143, (2000) · Zbl 0956.68055
[151] Cavaliere, M.; Sburlan, D., Time-independent P systems, (Proceedings of the 5th International Conference on Membrane Computing, WMC’04, (2005), Springer-Verlag Berlin, Heidelberg), 239-258 · Zbl 1117.68355
[152] Jensen, H. E., Model checking probabilistic real time systems, (Proceedings of the 7th Nordic Workshop on Programming Theory, (1996), Chalmers Institute of Technology), 247-261
[153] 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. · Zbl 0999.68125
[154] Kwiatkowska, M. Z.; Norman, G.; Sproston, J.; Wang, F., Symbolic model checking for probabilistic timed automata, Information and Computation, 205, 7, 1027-1077, (2007) · Zbl 1122.68075
[155] Kwiatkowska, M.; Norman, G.; Parker, D., PRISM 4.0: verification of probabilistic real-time systems, (Proceedings of the 23rd International Conference on Computer Aided Verification, LNCS, (2011), Springer)
[156] mcpta. URL http://www.modestchecker.net/.
[157] Shaw, A. C., Communicating real-time state machines, IEEE Transactions on Software Engineering, 18, 805-816, (1992)
[158] E. Posse, J. Dingel, Theory and implementation of a real-time extension to the \(\pi\)-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.
[159] Harel, D., Statecharts: a visual formalism for complex systems, Science of Computer Programming, 8, 3, 231-274, (1987) · Zbl 0637.68010
[160] Booch, G.; Maksimchuk, R.; Engle, M.; Young, B.; Conallen, J.; Houston, K., Object-oriented analysis and design with applications, third edition, (2007), Addison-Wesley Professional
[161] Alur, R.; Kannan, S.; Yannakakis, M., Communicating hierarchical state machines, (Proceedings of the 26th International Colloquium on Automata, Languages and Programming, ICAL’99, (1999), Springer-Verlag London, UK), 169-178
[162] Lanotte, R.; Maggiolo-Schettini, A.; Milazzo, P.; Troina, A., Design and verification of long-running transactions in a timed framework, Science of Computer Programming, 73, 76-94, (2008) · Zbl 1170.68024
[163] 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.
[164] Lanotte, R.; Maggiolo-Schettini, A.; Tini, S.; Peron, A., Transformations of timed cooperating automata, Fundamenta Informaticae, 47, 271-282, (2001) · Zbl 1004.68088
[165] Drusinsky, D.; Harel, D., On the power of bounded concurrency I: finite automata, Journal of the ACM, 41, 517-539, (1994) · Zbl 0813.68138
[166] Dima, C., Kleene theorems for event-clock automata, (Proceedings of the 12th International Symposium on Fundamentals of Computation Theory, FCT’99, (1999), Springer-Verlag London, UK), 215-225 · Zbl 0948.68106
[167] D’Souza, D., A logical characterisation of event recording automata, (Proceedings of the 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT’00, (2000), Springer-Verlag London, UK), 240-251 · Zbl 0986.68046
[168] D’Souza, D., A logical characterisation of event clock automata, International Journal Foundations Computer Science, 14, 4, 625-640, (2003) · Zbl 1101.68647
[169] M. Sorea, Tempo: a model-checker for event-recording automata, in: Proceedings of the 1st Workshop on Real-Time Tools, Aalborg, Denmark, August 2001.
[170] Penczek, W.; Woźna, B., Towards bounded model checking for timed automata, (Czaja, L., Proceedings of the International Workshop on Concurrency, Specification and Programming, CS&P’01, (2001), Warsaw University), 195-209
[171] Alur, R.; Madhusudan, P., Visibly pushdown languages, (Proceedings of the 36th Annual ACM Symposium on Theory of Computing, (2004), ACM Press), 202-211 · Zbl 1192.68396
[172] Chandra, A. K.; Kozen, D. C.; Stockmeyer, L. J., Alternation, Journal of the ACM, 28, 114-133, (1981) · Zbl 0473.68043
[173] Dickhöfer, M.; Wilke, T., Timed alternating tree automata: the automata-theoretic solution to the TCTL model checking problem, (Proceedings of the 26th International Colloquium on Automata, Languages and Programming, ICAL’99, (1999), Springer-Verlag London, UK), 281-290 · Zbl 0939.03041
[174] Ouaknine, J.; Worrell, J., On the decidability and complexity of metric temporal logic over finite words, Logical Methods in Computer Science, 3, 1, (2007) · Zbl 1128.03008
[175] Jenkins, M.; Ouaknine, J.; Rabinovich, A.; Worrell, J., Alternating timed automata over bounded time, (Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS’10, (2010), IEEE Computer Society Washington, DC, USA), 60-69
[176] Jones, N. D.; Landweber, L. H.; Lien, Y. E., Complexity of some problems in Petri nets, Theoretical Computer Science, 4, 277-299, (1977) · Zbl 0357.68048
[177] Gebremichael, B.; Vaandrager, F., Specifying urgency in timed I/O automata, (Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods, (2005), IEEE Computer Society Washington, DC, USA), 64-74
[178] Behrmann, G.; Cougnard, A.; David, A.; Fleury, E.; Larsen, K. G.; Didier, L., UPPAAL-tiga: time for playing games!, (Proceedings of the 19th International Conference on Computer Aided Verification, CAV’07, (2007), Springer-Verlag Berlin, Heidelberg), 121-125
[179] 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. · Zbl 1171.68526
[180] Henzinger, T. A.; Kopke, P. W., Discrete-time control for rectangular hybrid automata, Theoretical Computer Science, 221, 369-392, (1999) · Zbl 0930.68086
[181] 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. · Zbl 1171.68528
[182] 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.
[183] F. Cassez, N. Markey, Communicating Embedded Systems-Software and Design, Control of Timed Systems, pp. 83-120. 2009 (Chapter).
[184] Cassez, F.; Henzinger, T. A.; Raskin, J.-F., A comparison of control problems for timed and hybrid systems, (Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control, HSCC’02, (2002), Springer-Verlag London, UK), 134-148 · Zbl 1044.93518
[185] Daws, C.; Kordy, P., Symbolic robustness analysis of timed automata, (Asarin, E.; Bouyer, P., Proceedings of the 4th International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS’06, Lecture Notes in Computer Science, vol. 4202, (2006), Springer-Verlag), 143-155 · Zbl 1141.68429
[186] Swaminathan, M.; Franzle, M., A symbolic decision procedure for robust safety of timed systems, (Proceedings of the 14th International Symposium on Temporal Representation and Reasoning, (2007), IEEE Computer Society Washington, DC, USA), 192
[187] Dima, C., Dynamical properties of timed automata revisited, (Proceedings of the 5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS’07, (2007), Springer-Verlag Berlin, Heidelberg), 130-146 · Zbl 1142.68040
[188] Bouyer, P.; Markey, N.; Reynier, P.-A., Robust model-checking of linear-time properties in timed automata, (Correa, J. R.; Hevia, A.; Kiwi, M., Proceedings of the 7th Latin American Symposium on Theoretical Informatics, LATIN’06, Lecture Notes in Computer Science, vol. 3887, (2006), Springer Valdivia, Chile), 238-249 · Zbl 1145.68464
[189] 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. · Zbl 1326.68185
[190] Larsen, K. G.; Legay, A.; Traonouez, L.-M.; Wąsowski, A., Robust specification of real time components, (Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS’11, (2011), Springer-Verlag Berlin, Heidelberg), 129-144 · Zbl 1348.68143
[191] Ouaknine, J.; Worrell, J., Revisiting digitization, robustness, and decidability for timed automata, (Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, (2003), IEEE Computer Society Washington, DC, USA), 198-207
[192] 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.
[193] 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. · Zbl 1175.68240
[194] Abdulla, P. A.; Krcál, P.; Yi, W., Sampled semantics of timed automata, Logical Methods in Computer Science, 6, 3, (2010) · Zbl 1214.68195
[195] Bouyer, P.; Larsen, K. G.; Markey, N.; Sankur, O.; Thrane, C., Timed automata can always be made implementable, (Katoen, J.-P.; König, B., Proceedings of the 22nd International Conference on Concurrency Theory, CONCUR’11, Lecture Notes in Computer Science, vol. 6901, (2011), Springer Aachen, Germany) · Zbl 1343.68134
[196] Asarin, E.; Maler, O.; Pnueli, A., On discretization of delays in timed automata and digital circuits, (Proceedings of the 9th International Conference on Concurrency Theory, CONCUR’98, (1998), Springer-Verlag London, UK), 470-484 · Zbl 0933.94045
[197] Krčál, P.; Pelánek, R., On sampled semantics of timed systems, (Ramanujam, R.; Sen, S., Proceedings of the 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, vol. 3821, (2005), Springer-Verlag), 310-321 · Zbl 1172.68537
[198] Bosscher, D.; Polak, I.; Vaandrager, F. W., Verification of an audio control protocol, (Proceedings of the 3rd International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, (1994), Springer-Verlag London, UK), 170-192
[199] Wellings, A., Concurrent and real-time programming in Java, (2004), John Wiley & Sons
[200] 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.
[201] Hakimipour, N.; Strooper, P.; Wellings, A., TART: timed-automata to real-time Java tool, (Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM’10, (2010), IEEE Computer Society Washington, DC, USA), 299-309
[202] Jee, E.; Wang, S.; Kim, J. K.; Lee, J.; Sokolsky, O.; Lee, I., A safety-assured development approach for real-time software, (Proceedings of the 2010 IEEE 16th International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA’10, (2010), IEEE Computer Society Washington, DC, USA), 133-142
[203] 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.
[204] Ouimet, M.; Lundqvist, K., The TASM toolset: specification, simulation, and formal verification of real-time systems, (Proceedings of the 19th International Conference on Computer Aided Verification, CAV’07, (2007), Springer-Verlag Berlin, Heidelberg), 126-130
[205] Campana, S.; Spalazzi, L.; Spegni, F., XAL: a web oriented programming language based on timed-automata, (Proceedings of the 2008 IEEE/WIC/ACM International Conference on Web Intelligence and Intelligent Agent Technology — Volume 01, (2008), IEEE Computer Society Washington, DC, USA), 862-868
[206] Lv, M.; Guan, N.; Deng, Q.; Yu, G.; Yi, W., Mcait: a timing analyzer for multicore real-time software, (Proceedings of the 9th International Conference on Automated Technology for Verification and Analysis, ATVA’11, (2011), Springer-Verlag Berlin, Heidelberg), 414-417
[207] UPPAAL PRO. URL http://www.cs.aau.dk/ arild/uppaal-probabilistic/.
[208] Håkansson, J.; Carlson, J.; Monot, A.; Pettersson, P.; Slutej, D., Component-based design and analysis of embedded systems with UPPAAL PORT, (Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis, ATVA’08, (2008), Springer-Verlag Berlin, Heidelberg), 252-257
[209] 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.
[210] Larsen, K. G.; Mikucionis, M.; Nielsen, B.; Skou, A., Testing real-time embedded software using UPPAAL-TRON: an industrial case study, (Proceedings of the 5th ACM International Conference on Embedded Software, EMSOFT’05, (2005), ACM New York, NY, USA), 299-306
[211] 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.
[212] Sentilles, S.; Pettersson, A.; Nystrom, D.; Nolte, T.; Pettersson, P.; Crnkovic, I., Save-IDE — a tool for design, analysis and implementation of component-based embedded systems, (Proceedings of the 31st International Conference on Software Engineering, ICSE’09, (2009), IEEE Computer Society Washington, DC, USA), 607-610
[213] K. Altisen, S. Tripakis, Tools for controller synthesis of timed systems, in: Proceedings of the 2nd Workshop on Real-Time Tools, July 2002. · Zbl 1037.93522
[214] Closse, E.; Poize, M.; Pulou, J.; Sifakis, J.; Venter, P.; Weil, D.; Yovine, S., TAXYS: a tool for the development and verification of real-time embedded systems, (Proceedings of the 13th International Conference on Computer Aided Verification, CAV’01, (2001), Springer-Verlag London, UK), 391-395 · Zbl 0991.68644
[215] Tripakis, S.; Courcoubetis, C., Extending promela and spin for real time, (Proceedings of the 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems, (1996), Springer-Verlag London, UK), 329-348
[216] 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. · Zbl 1105.68352
[217] Laroussinie, F.; Larsen, K. G., CMC: a tool for compositional model-checking of real-time systems, (Proceedings of the FIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV XVIII), FORTE XI / PSTV XVIII’98, (1998), Kluwer, B.V Deventer, The Netherlands, The Netherlands), 439-456
[218] Kupferschmid, S.; Wehrle, M.; Nebel, B.; Podelski, A., Faster than UPPAAL?, (Proceedings of the 20th International Conference on Computer Aided Verification, CAV’08, (2008), Springer-Verlag Berlin, Heidelberg), 552-555
[219] Didier, J.-Y.; Djafri, B.; Klaudel, H., The \scmirela framework: modeling and analyzing mixed reality applications using timed automata, Journal of Virtual Reality and Broadcasting, 6, 1, (2009)
[220] Cambronero, M.-E.; Díaz, G.; Valero, V.; Martínez, E., Validation and verification of web services choreographies by using timed automata, Journal of Logic and Algebraic Programming, 80, 1, 25-49, (2011) · Zbl 1207.68082
[221] Bendiksen, L.; Ölveczky, P. C., The priced-timed maude tool, (Proceedings of the 3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO’09, (2009), Springer-Verlag Berlin, Heidelberg), 443-448
[222] Madl, G.; Dutt, N., Tutorial for the open-source \scdream tool. in CECS technical report, (2006)
[223] 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.
[224] Braberman, V. A.; Felder, M., Verification of real-time designs: combining scheduling theory with automatic formal verification, (Proceedings of the 7th European Software Engineering Conference held Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC/FSE-7, (1999), Springer-Verlag London, UK), 494-510
[225] Alfonso, A.; Braberman, V.; Kicillof, N.; Olivero, A., Visual timed event scenarios, (Proceedings of the 26th International Conference on Software Engineering, ICSE’04, (2004), IEEE Computer Society Washington, DC, USA), 168-177
[226] Braberman, V.; Garbervetsky, D.; Olivero, A., Obsslice: a timed automata slicer based on observers, (Proceedings of the 16th International Conference on Computer Aided Verification, LNCS, vol. 3114, (2004), Springer), 470-474 · Zbl 1103.68608
[227] Braberman, V.; Olivero, A.; Schapachnik, F., Issues in distributed timed model checking: building zeus, International Journal on Software Tools for Technology Transfer, 7, 4-18, (2005) · Zbl 1272.68231
[228] Larsen, K. G.; Pearson, J.; Weise, C.; Yi, W., Clock difference diagrams, Nordic Journal of Computing, 6, 271-298, (1999) · Zbl 0937.68086
[229] Asarin, E.; Bozga, M.; Kerbrat, A.; Maler, O.; Pnueli, A.; Rasse, A., Data-structures for the verification of timed automata, (Maler, O., Proceedings of the 1997 International Workshop on Hybrid and Real-Time Systems, HART’97, Lecture Notes in Computer Science, vol. 1201, (1997), Springer-Verlag), 346-360
[230] T. Wilke, Automaten und Logiken für zeitabhngige Systeme. Dissertation, Christian-Albrechts-Universität zu Kiel, 1994.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.