Modeling CHP Descriptions in Labeled Transitions Systems for an Efficient Formal Validation of Asynchronous Circuit Specifications
Menouer Boubekeur, D. Borrione, Laurent Mounier, Antoine Siriani, Marc Renaudin · Kluwer Academic Publishers eBooks · 2006
This work addresses the analysis and validation of CHP specifications for asynchronous circuits, using property Verification tools. CHP semantics, initially given in terms of Petri Nets, are reformulated as labeled transition systems. Circuit specifications are translated into an intermediate format (IF) based on communicating extended finite state machines. They are then validated using the IF environment, which provides model checking and bi-simulation tools. The direct translation must be optimized to delay state explosion. Performance studies are reported. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.