DiVinE: Parallel Distributed Model Checker (Tool paper)
DiVinE: Parallel Distributed Model Checker (Tool paper)
复制标题
DiVinE：并行分布式模型检查器（工具论文）
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Petr Ročkai
中科院分区：
文献类型：
--
作者：
J. Barnat;L. Brim;Milan Ceska;Petr Ročkai
模型检查已成为许多应用领域分析复杂系统的标准方法。毫无疑问，许多应用程序对模型检查工具提出了很高的要求。分析复杂和现实系统的过程通常需要大量的计算资源，特别是内存。这种现象，被称为状态空间爆炸问题，已经解决了许多研究人员在过去的二十年。已经引入了大量或多或少成功的技术来解决这个问题，包括并行和分布式内存处理。DIVINE是离散分布式系统LTL模型检测和可达性分析的工具。该工具能够有效地利用多个网络互连的多核工作站的聚合计算能力，以处理非常大的验证任务。因此，它允许分析的系统的大小远远超过系统的大小，可以处理与定期顺序工具。虽然该工具的主要重点是高性能显式状态模型检查，但重点也放在易于部署和使用上。此外，DIVINE的组件体系结构和公开源代码允许其作为一个平台，用于研究并行和分布式内存模型检查技术。
Model checking became a standard method of analysing complex systems in many application domains. No doubt, a number of applications is placing great demands on model checking tools. The process of analysis of complex and real-life systems often requires vast computation resources, memory in particular. This phenomenon, referred to as the state space explosion problem, has been tackled by many researchers during the past two decades. A plethora of more or less successful techniques to fight the problem have been introduced, including parallel and distributed-memory processing. DIVINE is a tool for LTL model checking and reachability analysis of discrete distributed systems. The tool is able to efficiently exploit the aggregate computing power of multiple network-interconnected multi-cored workstations in order to deal with extremely large verification tasks. As such it allows to analyse systems whose size is far beyond the size of systems that can be handled with regular sequential tools. While the main focus of the tool is on highperformance explicit state model checking, an emphasis is also put on ease of deployment and usage. Additionally, the component architecture and publicly available source code of DIVINE allow for its usage as a platform for research on parallel and distributedmemory model checking techniques.