关键词: 交互, 形式化语义, 组合定义, 线性化

Abstract: Interaction in UML2 brings up a new traces based semantics which makes up the lack of semantics in its earlier version. Unfortunately, the new semantics is described in natural language and there are so many details that are not explained clearly and completely enough to get a good understanding of an interaction. This paper formalizes this traces based semantics with set theory in a compositional way. Moreover, it proves the semantics of an interaction is a preordered set. And the linearization of the preordered set is exactly the traces set of the interaction defined in the specification. The formalized semantics is a key supplement to the specification of interactions in UML2. It can be useful in the understanding of interactions in UML2. And it lays a solid foundation for the applications and researches of interactions in UML2.

Key words: interaction, formal semantics, composite definition, linearization