Refinement of UML Interaction for Correct Embedded System Design

Correctness is the crucial issue in the design of safety-critical embedded systems. In order to guarantee the correct system design, a restricted refinement relation is represented in this paper for UML Interaction models.Both the basic and the combined interactions are defined in terms of partially ordered multisets formalism, from which the trace semantics is derived. A number of algebraic refinement laws are provided, allowing us to refine an abstract Interaction model in a compositional way. We also justify the proposed refinement relation by proving that it implies both action refinement of event structures and trace refinement of CSP.