Gómez, Rodolfo Model-checking timed automata with deadlines with Uppaal. (English) Zbl 1259.68126 Formal Asp. Comput. 25, No. 2, 289-318 (2013). MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 68Q05 Models of computation (Turing machines, etc.) (MSC2010) Keywords:real-time systems; model-checking; urgent actions; timed automata with deadlines Software:MOTOR; MoDeST; Kronos; Uppaal; IF-2.0 PDFBibTeX XMLCite \textit{R. Gómez}, Formal Asp. Comput. 25, No. 2, 289--318 (2013; Zbl 1259.68126) Full Text: DOI References: [1] Aceto L, Bouyer P, Burgueño A, Larsen K (2003) The power of reachability testing for timed automata. Theor Comput Sci 300(1–3): 411–475 · Zbl 1023.68060 [2] Alur R, Dill D (1994) A theory of timed automata. Theor Comput Sci 126: 183–235 · Zbl 0803.68071 [3] Blair GS, Blair L, Bowman H et al (1998) Formal specification of distributed multimedia systems. UCL Press [4] Bohnenkamp H, D’Argenio PR, Hermanns H, Katoen J-P (2006) Modest: a compositional modeling formalism for hard and softly timed systems. IEEE Trans Softw Eng 32(10): 812–830 · Zbl 05341944 [5] Behrmann G, David A, Larsen K (2004) A tutorial on Uppaal. In: SFM-RT 2004. LNCS 3185, pp 200–236. Springer, New York · Zbl 1105.68350 [6] Bowman H, Faconti G, Katoen J-P, Latella D, Massink M (1998) Automatic verification of a lip synchronization protocol using uppaal. Form Asp Comput 10(5–6): 550–575 · Zbl 0951.68533 [7] Bowman H, Gomez R (2006) Concurrency theory, calculi and automata for modelling untimed and timed concurrent systems. Springer, Berlin · Zbl 1140.68046 [8] Bozga M, Graf S, Ober I, Ober I, Sifakis J (2004) The IF toolset. In: SFM-RT 2004. LNCS, vol 3185. Springer, Berlin, pp 237–267 · Zbl 1105.68352 [9] Bohnenkamp HC, Hermanns H, Katoen J-P (2007) MOTOR: the MODEST tool environment. In: TACAS’07. LNCS, vol 4424, pp 500–504. Springer, Berlin [10] Bowman H (2001) Time and action lock freedom properties for timed automata. In: Proceedings of FORTE 2001. Kluwer, Dordrecht, pp 119–134 [11] Bornot S, Sifakis J (1998) On the composition of hybrid systems. In: Hybrid systems: computation and control. LNCS, vol 1386. Springer, Berlin, pp 49–63 [12] Bornot S, Sifakis J, Tripakis S (1998) Modeling urgency in timed systems. In: Proceedings of COMPOS 1997. LNCS, vol 1536. Springer, Berlin, pp 103–129 [13] Barbuti R, Tesei L (2004) Timed automata with urgent transitions. Acta Inf 40(5): 317–347 · Zbl 1072.68053 [14] Gomez R (2008) Verification of timed automata with deadlines in Uppaal. TR 2-08-2008, Computing Laboratory, University of Kent [15] Gomez R (2009) A compositional translation from timed automata with deadlines to Uppaal timed automata. In: 7th international conference on formal modelling and analysis of timed systems (FORMATS’09). LNCS, vol 5813, Budapest, Hungary, September 2009. Springer, Berlin, pp 179–194 [16] Gebremichael B, Vaandrager F, Zhang M (2006) Analysis of the zeroconf protocol using Uppaal. In: EMSOFT ’06. ACM Press, pp 242–251 [17] Henzinger T, Nicollin X, Sifakis J, Yovine S (1994) Symbolic model checking for real-time systems. Inf Comput 111(2): 193–244 · Zbl 0806.68080 [18] Havelund K, Skou A, Larsen KG, Lund K (1997) Formal modeling and analysis of an audio/video protocol: an industrial case study using Uppaal. In: IEEE real-time systems symposium, RTSS ’97. IEEE Computer Society, pp 2–13 [19] Kozen D (1983) Results on the propositional mu-calculus. Theor Comput Sci 27: 333–354 · Zbl 0553.03007 [20] Lindahl M, Pettersson P, Yi W (2001) Formal design and analysis of a gearbox controller. Softw Tools Technol Transf 3(3): 353–368 · Zbl 0993.68133 [21] Moller F, Tofts C (1990) A temporal calculus of communicating systems. In: Proceedings of CONCUR 1990. Springer, New York, pp 401–415 [22] Sifakis J, Yovine S (1996) Compositional specification of timed systems. In: Proceedings of STACS’96. LNCS, vol 1046. Springer, Berlin, pp 347–359 · Zbl 1379.68240 [23] Tripakis S, Yovine S (2001) The analysis of timed systems using time-abstracting bisimulations. Form Methods Syst Des 18(1): 25–68 · Zbl 0971.68096 [24] Vaandrager F, de Groot A (2006) Analysis of a biphase mark protocol with Uppaal and PVS. Form Asp Comput 18(4): 433–458 · Zbl 1102.68505 [25] Yovine S (1997) Kronos: a verification tool for real-time systems. Int J Softw Tools Technol Transf 1(1–2): 123–133 · Zbl 1060.68606 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.