Automated refinement checking of concurrent systems

Stepwise refinement is at the core of many approaches to synthesis and optimization of hardware and software systems. For instance, it can be used to build a synthesis approach for digital circuits from high level specifications. It can also be used for post-synthesis modification such as in Engineering Change Orders (ECOs). Therefore, checking if a system, modeled as a set of concurrent processes, is a refinement of another is of tremendous value. In this paper, we focus on concurrent systems modeled as Communicating Sequential Processes (CSP) and show their refinements can be validated using insights from translation validation, automated theorem proving and relational approaches to reasoning about programs. The novelty of our approach is that it handles 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...

• Type: Conference
• Year: 2007
• Where: ICCAD
• Authors: Sudipta Kundu, Sorin Lerner, Rajesh Gupta
• Keywords: Hardware, ICCAD 2007, Infinite State Space, Refinement Checking Technique, Stepwise Refinement