论 GPUexplore 显式状态模型检测器的可扩展性
分布式、并行与集群计算
2018-01-19 v1 数据结构与算法
摘要
使用图形处理器（GPU）是一种有前景的方法，可加速模型检测至在开发过程中即时验证软件系统可行的程度。GPUexplore是一个将其所有计算都在GPU上运行的显式状态模型检测器。多年来它已扩展多种技术，且持续提升其性能的可能性被不断研究。本文讨论该工具哈希表的工作机制，这是其功能的核心。我们提出一种在隔离实验中看似有前景的哈希表改动，并分析其集成到工具中的效果。此外，我们通过在大小各异的输入模型上实验并在NVIDIA最新GPU之一上运行该工具，研究GPUexplore当前的可扩展性。
引用
@article{arxiv.1801.05857,
title = {On the Scalability of the GPUexplore Explicit-State Model Checker},
author = {Nathan Cassee and Thomas Neele and Anton Wijs},
journal= {arXiv preprint arXiv:1801.05857},
year = {2018}
}
备注
In Proceedings GaM 2017, arXiv:1712.08345