利用稠密时间模型检测技术验证实时提交协议
软件工程
2018-05-11 v2
摘要
由 Alur 和 Dill 引入的基于时间的自动机模型为描述实时系统提供了一种有用的形式化方法。在过去的二十年里，基于该模型开发了几种稠密时间模型检测工具。本文考虑利用稠密时间模型检测技术对实时分布式提交协议进行验证。更具体地说，我们在三种最先进的实时模型检测器 UPPAAL、Rabbit 和 RED 中对著名的定时两阶段提交协议进行了建模和验证，并比较了结果。
引用
@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}
}