text: The timed-based automata model, introduced by Alur and Dill, provides a useful formalism for describing real-time systems. Over the last two decades, several dense-time model checking tools have been developed based on that model. The paper considers the verification of real-time distributed commit protocols using dense-time model checking technology. More precisely, we model and verify the well-known timed two phase commit protocol in three different state-of-the-art real-time model checkers: UPPAAL, Rabbit, and RED, and compare the results.
  @cite_21: Finite automata and regular languages have been useful in a wide variety of problems in computing, communication and control, including formal modeling and verification. Traditional automata do not admit an explicit modeling of time, and consequently, timed automata [2] were introduced as a formal notation to model the behavior of real-time systems. Timed automata accept timed languages consisting of sequences of events tagged with their occurrence times. Over the years, the formalism has been extensively studied leading to many results establishing connections to circuits and logic, and much progress has been made in developing verification algorithms, heuristics, and tools. This paper provides a survey of the theoretical results concerning decision problems of reachability, language inclusion and language equivalence for timed automata and its variants, with some new proofs and comparisons. We conclude with a discussion of some open problems.
  @cite_13: An impact-proof watchcase having a watchcase band with an internal shoulder. A watchcase inner ring is provided within the band within which is disposed a ring supporting a dial and watchworks internally thereof. An impact-absorbing member is disposed between the inner shoulder and the ring supporting the dial for absorbing impacts on the watchcase. A watch crystal is provided for viewing the dial and a bezel is disposed circumferentially of the watch crystal. A second impact-absorbing member is disposed cooperative with the watchcase inner ring and provides an elastic support therefore for absorbing shocks to which the watchworks are subjected. The impact-absorbing members absorb movements or vibrations in three dimensions.
summary: The literature of timed automata theory is a rich literature since it was introduced by Alur and Dill in 1990. Alur and Madhusudan @cite_21 present a full survey of known results for decidability problems in timed automata theory. Tripakis @cite_13 gives algorithms and techniques to verify timed systems using TCTL logic and Timed Buchi Automata, which have implemented in KRONOS model checking tool. One of the disadvantages of KRONOS is that its input language supports a very restricted data types that allow only the declaration of clock variables. For this reason we have not included KRONOS in our comparative study.