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

fYear

2012

fDate

12-14 Sept. 2012

Firstpage

65

Lastpage

72

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Temporal Representation and Reasoning (TIME), 2012 19th International Symposium on

Conference_Location

Leicester

ISSN

1530-1311

Print_ISBN

978-1-4673-2659-9

Type

conf

DOI

10.1109/TIME.2012.12

Filename

6311116