We present a formal analysis of the well-known two phase atomic commitment protocol. The protocol is modeled as networks of timed automata using the model checker UPPAAL. The protocol has been verified in two different crash models, the crash-stop model, and the crash-recovery model. The paper also describes how dense-timed model checking technology may be applied to discover the worst case execution time and the corresponding worst-case scenario of the protocol. The analysis also allows us to illustrate various features of the UPPAAL tool, which shows that the specification language of the tool lacks the expressiveness to capture some desired properties of the protocol.
展开▼
