A Comparative Study of Decision Diagrams for Real-Time Model Checking.
Lecture Notes in Computer Science(2018)
摘要
The timed automata model, introduced by Alur and Dill, provides a powerful formalism for describing real-time systems. Over the last two decades, several dense-time model checking tools have been developed based on that model. This paper considers the verification of a set of interesting real-time distributed protocols using dense-time model checking technology. More precisely, we model and verify the distributed timed two phase commit protocol, and two well-known benchmarks, the Token-Ring-FDDI protocol, and the CSMA/CD protocol, in three different state-of-the-art real-time model checkers: UPPAAL, RED, and Rabbit. We illustrate the use of these tools using one of the case studies. Finally, several interesting conclusions have been drawn about the performance, usability, and the capability of each tool.
更多查看译文
关键词
decision diagrams,model,real-time
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络