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

Omar I. Al-Bataineh, Mark Reynolds

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 check…