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

摘要： UML2（unified modeling language 2.x）的规范为其交互定义了一种基于事件发生轨迹的语义，弥补了之前版本在语义上的欠缺。但是此语义是用自然语言（英语）描述的，不够精确、不一致，并且很多细节解释得不够清楚和完备。利用集合论以组合定义的方式形式化语义，并且证明了形式化后交互的语义为拟序集，此拟序集的线性化恰好就是规范所定义的轨迹集。此形式化语义可以作为UML2交互规范的很好的补充，不但有助于UML2交互的理解，还为UML2交互的应用和研究奠定了坚实的理论基础。

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