  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.
