Swarm Verification
Swarm Verification
复制标题
集群验证
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Alex Groce
中科院分区：
文献类型：
--
作者：
G. Holzmann;Rajeev Joshi;Alex Groce
据报道，超级计算机设计师西摩·克雷曾说，他宁愿用两头强壮的牛耕地，也不愿用一千只鸡耕地。虽然这在耕地时无疑是明智的，但对于其他类型的任务就不那么清楚了。模型检验问题是众所周知的“大海捞针”类型。这类问题通常可以很容易地并行化。唉，没有一个常用的分治方法可以用来并行化模型检查器的工作。考虑到访问大量计算机来执行甚至是例行任务比以往任何时候都更容易，找到使用这些资源来加速模型检查任务的替代方法变得越来越有吸引力。本文介绍了一种这样的方法，称为群验证。
Reportedly, supercomputer designer Seymour Cray once said that he would sooner use two strong oxen to plow afield than a thousand chickens. Although this is undoubtedly wise when it comes to plowing afield, it is not so clear for other types of tasks. Model checking problems are of the proverbial "search the needle in a haystack" type. Such problems can often be parallelized easily. Alas, none of the usual divide and conquer methods can be used to parallelize the working of a model checker. Given that it has become easier than ever to gain access to large numbers of computers to perform even routine tasks it is becoming more and more attractive to find alternate ways to use these resources to speed up model checking tasks. This paper describes one such method, called swarm verification.