Handshaking Expansion Based on Action Refinement

Handshaking expansion is a main procedure in the design of asynchronous circuits. At present, there is not description and definition for the refinement of handshaking expansion formality. Through investigating formal semantics of the handshaking expansion of asynchronous circuits, a refinement model for handshaking expansion is presented based on a powerful strategy of action refinement in the hierarchical design of concurrent systems. The proposed semantics employs wait event structures and then derives a true concurrency model with maximum parallelism. The refined system conforms to the original specification with respect to a vertical bisimulation relation. Furthermore, the refinement function preserves correctness and deadlock-freeness of the behavior in the refined system.