Communicating Sequential Processes (CSP) is a calculus for describing concurrent systems as a collection of processes communicating over channels. Checking that one CSP program is a refinement of another has many applications, including type-checking concurrent systems, and refinement-based synthesis and optimization of hardware circuits. In this paper, we describe a new approach to automatic refinement checking of CSP programs that uses insights from translation validation, automated theorem proving, and relational approaches to reasoning about programs. Unlike previous approaches to CSP refinement, our technique can handle infinite state spaces in a fully automated manner. We have implemented our refinement checking technique and have applied it to a variety of refinements. We present the details of our algorithm and experimental results. As an example, we were able to automatically check an infinite state space buffer refinement that cannot be checked by current state of the art tools such as FDR. We were also able to check the data part of an industrial case study on the EP2 system.
The authors of these documents have submitted their reports to this technical report series for the purpose of non-commercial dissemination of scientific work. The reports are copyrighted by the authors, and their existence in electronic format does not imply that the authors have relinquished any rights. You may copy a report for scholarly, non-commercial purposes, such as research or instruction, provided that you agree to respect the author's copyright. For information concerning the use of this document for other than research or instructional purposes, contact the authors. Other information concerning this technical report series can be obtained from the Computer Science and Engineering Department at the University of California at San Diego, firstname.lastname@example.org.
[ Search ]