Effective State Exploration for Model Checking on a Shared Memory Architecture Cornelia P. Inggs and Howard Barringer
In this paper we present results from experimental studies
investigating implementation strategies for explicit-state
temporal-logic model checking on a virtual shared-memory
high-performance parallel machine architecture. In
particular, a parallel state exploration algorithm using a
two-queue structure for load balancing is proposed and its
performance analysed at the hand of experimental studies.
We then discuss implementation issues for parallel
automata-theoretic model checking using this parallel state
exploration algorithm.
|