Sciweavers

ICCAD
2007
IEEE

Automated refinement checking of concurrent systems

13 years 7 months ago
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...
Sudipta Kundu, Sorin Lerner, Rajesh Gupta
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2007
Where ICCAD
Authors Sudipta Kundu, Sorin Lerner, Rajesh Gupta
Comments (0)