Discrete Timed Automata

Book English OPEN
Gomez, Rodolfo ; Bowman, Howard (2005)
  • Publisher: UKC
  • Subject: QA76

MONA implements an efficient decision procedure for the logic WS1S, and has already been applied in many non-trivial problems. Among these, we follow on from previous work done by Smith and Klarlund on the verification of a sliding-window protocol. One of the goals of this paper is to extend the scope of MONA to the verification of time-dependent protocols. We present Discrete Timed Automata (DTA) as a suitable formalism to specify and verify such protocols, and (discrete, infinite-state) real-time systems in general. DTA are as much influenced by IO Automata (syntactically) as they are by Timed Automata (semantically). However, DTA presents a number of distinctive features. Among them, urgency conditions can be directly related to actions, and they are constrained in such a way that time-actionlocks are ruled out by construction. A composition strategy is given to combine a set of synchronising automata, resulting in a product automaton over which safety properties can be verified. Invariance proofs are then performed inductively on the automaton structure, and mechanically assisted by MONA. Therefore, this paper also aims to study benefits and weaknesses of DTA as a real-time formalism, compared with existent frameworks such as Timed IO Automata, TLA+ and Clocked Transition Systems. Our case study will be the specification and verification of a multimedia stream protocol. This is compared to previous work where the formalisation of the protocol is realised in UPPAAL.
  • References (27)
    27 references, page 1 of 3

    [9] S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. In Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures, LNCS 1536, pages 103-129. Springer, 1998.

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

    [11] H. Bowman, G. Faconti, and M. Massink. Specification and verification of media constraints using uppaal. In 5th Eurographics Workshop on the Design, Specification and Verification of Interactive Systems, DSVIS 98, Eurographics Series. Springer-Verlag, August 1998.

    [12] H. Bowman, R. Go´mez, and L. Su. A tool for the syntactic detection of zeno-timelocks in timed automata. In Proceedings of the 6th AMAST Workshop on Real-Time Systems, Stirling, July 2004.

    [13] Howard Bowman. Time and action lock freedom properties for timed automata. In S. Kang M. Kim, B. Chin and D. Lee, editors, FORTE 2001, Formal Techniques for Networked and Distributed Systems, pages 119-134, Cheju Island, Korea, 2001. Kluwer Academic Publishers.

    [14] M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A model-checking tool for real-time systems. In Proceedings of the 10th International Conference on Computer Aided Verification, pages 546-550. Springer-Verlag, 1998.

    [15] J. R. Bu¨chi. On a decision method in restricted second-order arithmetic. Zeitschrift fu¨r Mathemathische Logik and Grundlagen der Mathematik, 6:66-92, 1960.

    [16] C. C. Elgot. Decision Problems of Finite Automata Design and Related Arithmetics. Trans. Amer. Math. Soc., 98:21-51, 1961.

    [17] U. Engberg, P. Gronning, and L. Lamport. Mechanical verification of concurrent systems with TLA. In Computer Aided Verification, pages 44-55, 1992.

    [18] R. Gawlick, R. Segala, J. F. Sogaard-Andersen, and N. A. Lynch. Liveness in timed and untimed systems. In Automata, Languages and Programming, pages 166-177, 1994.

  • 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 10
Share - Bookmark