Automated Refinement Checking for Asynchronous Processes

Abstract. 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 base...

• Type: Conference
• Year: 2000
• Where: FMCAD
• Authors: Rajeev Alur, Radu Grosu, Bow-Yaw Wang
• Keywords: FMCAD 2000, Formal Methods, Individual Refinement Checks, Refinement Check, Refinement Checking