Journal
FORMAL METHODS IN SYSTEM DESIGN
Volume 29, Issue 2, Pages 157-175Publisher
SPRINGER
DOI: 10.1007/s10703-006-0011-4
Keywords
distributed reachability; symbolic model checking; distributed BDDs; splitting; load balance
Categories
Ask authors/readers for more resources
This work presents a novel distributed symbolic algorithm for reachability analysis that can effectively exploit, as needed, a large number of machines working in parallel. The novelty of the algorithm is in its dynamic allocation and reallocation of processes to tasks and in its mechanism for recovery from local state explosion. As a result, the algorithm is work-efficient: it utilizes only those resources that are actually needed. In addition, its high adaptability makes it suitable for exploiting the resources of very large and heterogeneous distributed, nondedicated environments. Thus, it suitable for verifying very large systems. We implemented our algorithm in a tool called Division. Our experimental results show that the algorithm is indeed work-efficient. Although the goal of this research is to check larger models, the results also indicate that the algorithm can obtain high speedups, because communication overhead is very small.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available