Title :
Formal Modeling and Analysis of a Distributed Transaction Protocol in UPPAAL
Author :
Al-Bataineh, Omar ; French, Tim ; Woodings, Terry
Author_Institution :
Univ. of Western Australia, Crawley, WA, Australia
Abstract :
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.
Keywords :
automata theory; distributed processing; formal specification; program diagnostics; transaction processing; UPPAAL; crash-recovery model; crash-stop model; dense-timed model checking technology; distributed transaction protocol; formal analysis; formal modeling; model checker; specification language; timed automata; two phase atomic commitment protocol; worst case execution time; worst-case scenario; Analytical models; Automata; Clocks; Computer crashes; Protocols; Timing;
Conference_Titel :
Temporal Representation and Reasoning (TIME), 2012 19th International Symposium on
Conference_Location :
Leicester
Print_ISBN :
978-1-4673-2659-9
DOI :
10.1109/TIME.2012.12
