We consider the problem of refinement checking for asynchronous processes
where refinement corresponds to stutter-closed language inclusion.
Since an efficient algorithmic solution to the refinement check
demands the construction of a "witness" that
defines the private specification variables in terms of the
implementation variables, we first propose a construction
to extract a synchronous witness from the specification.
This automatically reduces individual refinement checks to
reachability analysis.
Second, to alleviate the state-explosion problem during search,
we propose a reduction scheme that exploits the visibility information
about transitions in a recursive manner based on the architectural
hierarchy. Third, we establish compositional and assume-guarantee
proof rules for decomposing the refinement check into subproblems.
All these techniques work in synergy to reduce the computational
requirements of refinement checking.
We have integrated the proposed methodology based on an enumerative
checker. We illustrate our approach on sample benchmarks.
