A coordinated reachability analysis method for modular verification of asynchronous designs

Divide-and-conquer is essential to address state explosion in model checking. Traditionally, an over-approximate context is required when verifying each individual component in a system. This may cause state explosion for the intermediate results as well as inefficiency for abstraction refinement. This paper presents an opposite approach, a coordinated reachability analysis method, that constructs state space of each component from an under-approximate context gradually until a counter-example is found or a fix-point in state space is reached. This method has an additional advantage in that counter-examples, if there are any, can be found much earlier leading to faster verification. Furthermore, this modular verification framework does not require complex compositional reasoning rules. The experimental results indicate that this method is promising.