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.
Proceedings of the 9th International Conference for Young Computer Scientists (ICYCS 2008), Zhang Jia Jie, China, 18-21 November 2008 / Guojun Wang, Jianer Chen, Michael R. Fellows and Huadong Ma (eds.),