Verifying Real-time Commit Protocols Using Dense-time Model Checking Technology
Software Engineering
2018-05-11 v2
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.
Cite
@article{arxiv.1201.3416,
title = {Verifying Real-time Commit Protocols Using Dense-time Model Checking Technology},
author = {Omar I. Al-Bataineh and Mark Reynolds},
journal= {arXiv preprint arXiv:1201.3416},
year = {2018}
}