Verification of Timed Automata with Deadlines in Uppaal

Book English OPEN
Gomez, Rodolfo (2008)
  • Publisher: UKC
  • Subject: QA76

Timed Automata with Deadlines (TAD) is a notation to model concurrent real-time systems that has a number of advantages over mainstream Timed Automata (TA). The semantics of deadlines and synchronisation rule out the most common form of timelocks, making TAD more robust than TA w.r.t. formal verification. In addition, it is often the case that urgency is more naturally expressed with deadlines rather than invariants. However, with the exception of the IF Toolset, there are no real-time model-checkers which support TAD models. This paper extends the available tool support by offering a compositional translation from TAD networks to Uppaal's TA networks. The techniques presented in this paper allow users to benefit from Uppaal's GUI, modelling facilities and efficient verification algorithms to construct and analyze TAD models.
  • References (23)
    23 references, page 1 of 3

    [1] L. Aceto, P. Bouyer, A. BurguenĖœo, and K. Larsen. The power of reachability testing for timed automata. Theoretical Computer Science, 1-3(300):411-475, 2003.

    [2] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994.

    [3] R. Barbuti and L. Tesei. Timed automata with urgent transitions. Acta Informatica, 40(5), March 2004.

    [4] G. Behrmann, A. David, and K. Larsen. A tutorial on Uppaal. In SFM-RT 2004, LNCS 3185, pages 200-236. Springer, 2004.

    [5] H. C. Bohnenkamp, H. Hermanns, and J-P. Katoen. MOTOR: The MODEST tool environment. In TACAS'07, LNCS 4424, pages 500-504. Springer, 2007.

    [6] S. Bornot and J. Sifakis. On the composition of hybrid systems. In Hybrid Systems: Computation and Control, LNCS 1386, pages 49-63. Springer, 1998.

    [7] S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. In Proc. of COMPOS 1997, LNCS 1536, pages 103-129. Springer, 1998.

    [8] H. Bowman. Time and action lock freedom properties for timed automata. In Proceedings of FORTE 2001, pages 119-134. Kluwer Academic, 2001.

    [9] H. Bowman, G. Faconti, J.-P. Katoen, D. Latella, and M. Massink. Automatic verification of a lip synchronization protocol using uppaal. Formal Aspects of Computing, 10(5-6):550-575, August 1998.

    [10] H. Bowman and R. Gomez. Concurrency Theory, Calculi and Automata for Modelling Untimed and Timed Concurrent Systems. Springer, January 2006.

  • Metrics
    views in OpenAIRE
    views in local repository
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    Kent Academic Repository - IRUS-UK 0 16
Share - Bookmark