Swarm verification and parallel randomised depth-first search are very effective parallel techniques to hunt bugs in large explicit state spaces. In case bugs are absent, however, scalability of the parallelisation is completely lost. Informed swarm verification is an extension, in which workers periodically communicate with a manager to perform bounded searches. The workers do not synchronise with each other, though. This scheme helps each worker to perform a finite search, even if the state space is infinitely large, while still benefitting from randomisation to find bugs quickly. Because the workers operate independently, this technique is very suitable for large-scale parallel explicit state space exploration on a computer cluster. A prototype of this technique has been implemented in the LTSmin toolset, developed at the University of Twente.
|Title of host publication
|Proceedings of the 13th International Workshop on Verification of Infinite-State Systems, October 10, 2011, Taipei, Taiwan
|Place of Publication
|Open Publishing Association
|Published - 2011
|Electronic Proceedings in Theoretical Computer Science