Gómez, Rodolfo A compositional translation of timed automata with deadlines to Uppaal timed automata. (English) Zbl 1262.68091 Ouaknine, Joël (ed.) et al., Formal modeling and analysis of timed systems. 7th international conference, FORMATS 2009, Budapest, Hungary, September 14–16, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04367-3/pbk). Lecture Notes in Computer Science 5813, 179-194 (2009). Summary: Timed automata with deadlines (TAD) are a form of timed automata that admit a more natural representation of urgent actions, with the additional advantage of avoiding the most common form of timelocks. We offer a compositional translation of a practically useful subset of TAD to timed safety automata (the well-known variant of timed automata where time progress conditions are expressed by invariants). More precisely, we translate networks of TAD to the modeling language of Uppaal, a state-of-the-art verification tool for timed automata. We also describe an implementation of this translation, which allows Uppaal to aid the design and analysis of TAD models.For the entire collection see [Zbl 1176.68014]. Cited in 1 Document MSC: 68Q45 Formal languages and automata 68Q60 Specification and verification (program logics, model checking, etc.) Keywords:urgent actions; timed automata with deadlines; Uppaal Software:PVS; Uppaal; MoDeST; Kronos; MOTOR; IF-2.0 PDFBibTeX XMLCite \textit{R. Gómez}, Lect. Notes Comput. Sci. 5813, 179--194 (2009; Zbl 1262.68091) Full Text: DOI References: [1] Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994) · Zbl 0803.68071 [2] Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation 111(2), 193–244 (1994) · Zbl 0806.68080 [3] Yovine, S.: Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1(1-2), 123–133 (1997) · Zbl 1060.68606 [4] Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004) · Zbl 1105.68350 [5] Bowman, H.: Time and action lock freedom properties for timed automata. In: Proceedings of FORTE 2001, pp. 119–134. Kluwer Academic Publishers, Dordrecht (2001) [6] Bowman, H., Gomez, R.: How to stop time stopping. Formal Aspects of Computing 18(4), 459–493 (2006) · Zbl 1105.68059 [7] Sifakis, J., Yovine, S.: Compositional specification of timed systems. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 347–359. Springer, Heidelberg (1996) · Zbl 1379.68240 [8] Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 103–129. Springer, Heidelberg (1998) [9] Bowman, H., Faconti, G., Katoen, J.P., Latella, D., Massink, M.: Automatic verification of a lip synchronization protocol using uppaal. Formal Aspects of Computing 10(5-6), 550–575 (1998) · Zbl 0951.68533 [10] Bornot, S., Sifakis, J.: On the composition of hybrid systems. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol. 1386, pp. 49–63. Springer, Heidelberg (1998) [11] Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: The IF toolset. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 237–267. Springer, Heidelberg (2004) · Zbl 1105.68352 [12] Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983) · Zbl 0553.03007 [13] Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.: The power of reachability testing for timed automata. Theoretical Computer Science 1-3(300), 411–475 (2003) · Zbl 1023.68060 [14] D’Argenio, P.R., Hermanns, H., Katoen, J.-P., Klaren, R.: MoDeST - a modelling and description language for stochastic timed systems. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 87–104. Springer, Heidelberg (2001) · Zbl 1007.68518 [15] Bohnenkamp, H.C., Hermanns, H., Katoen, J.-P.: MOTOR: The MODEST tool environment. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 500–504. Springer, Heidelberg (2007) · Zbl 05185798 [16] Barbuti, R., Tesei, L.: Timed automata with urgent transitions. Acta Informatica 40(5) (March 2004) · Zbl 1072.68053 [17] Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401–415. Springer, Heidelberg (1990) [18] Gomez, R.: Verification of Timed Automata with Deadlines in Uppaal. TR 2-08-2008, Computing Laboratory, University of Kent (2008) [19] Bowman, H., Gomez, R.: Concurrency Theory, Calculi and Automata for Modelling Untimed and Timed Concurrent Systems. Springer, Heidelberg (2006) · Zbl 1140.68046 [20] Tripakis, S., Yovine, S.: The analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18(1), 25–68 (2001) · Zbl 0971.68096 [21] Gebremichael, B., Vaandrager, F., Zhang, M.: Analysis of the zeroconf protocol using Uppaal. In: EMSOFT 2006, pp. 242–251. ACM Press, New York (2006) [22] Vaandrager, F., de Groot, A.: Analysis of a biphase mark protocol with Uppaal and PVS. Formal Aspects of Computing 18(4), 433–458 (2006) · Zbl 1102.68505 [23] Lindahl, M., Pettersson, P., Yi, W.: Formal design and analysis of a gearbox controller. Software Tools for Technology Transfer (STTT) 3(3), 353–368 (2001) · Zbl 0993.68133 [24] Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio/video protocol: an industrial case study using Uppaal. In: IEEE Real-Time Systems Symposium, RTSS 1997, pp. 2–13. IEEE Computer Society, Los Alamitos (1997) 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.