Handshaking expansion as action refinement

This paper presents a formal refinement model for handshaking expansion based on a powerful strategy of action refinement in the hierarchical design of concurrent systems. The proposed methodology employs wait event structures. It derives a true concurrency model with maximum parallelism, and the refined system conforms to the original specification with respect to a vertical bisimulation relation. Furthermore, the refinement function can preserve correctness and deadlock-freeness of the behavior in the refined system.