Verifying Real-time Commit Protocols Using Dense-time Model Checking Technology

TL;DR

This paper evaluates the effectiveness of dense-time model checking tools in verifying real-time distributed commit protocols, specifically modeling and analyzing the timed two-phase commit protocol across three different tools.

Contribution

It provides a comparative analysis of UPPAAL, Rabbit, and RED in verifying real-time commit protocols using dense-time automata models.

Findings

All three tools successfully verified the protocol properties.

Performance and scalability varied among the tools.

The study highlights strengths and limitations of each model checker.

Abstract

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.