Combining hierarchical specification with hierarchical implementation, in

Abstract. Action refinement is a practical hierarchical method to ease the design of large reactive systems. Relating hierarchical specification to hierarchical implementation is an effective method to decrease the complexity of the verification of these systems. In our previous work [15], this issue has been investigated in the simple case of the refinement of an action by a finite process. In this paper, on the one hand, we extend our previous results by consid-ering the issue in general, i.e., refining an abstract action by an arbitrary process; on the other hand, we exploit different techniques such that our method is easier to be followed and applied in practice