Journal of Frontiers of Computer Science and Technology ›› 2012, Vol. 6 ›› Issue (7): 631-643.DOI: 10.3778/j.issn.1673-9418.2012.07.007

Previous Articles     Next Articles

A Formal Semantics for Interactions in UML2

GU Sishan1+, CAI Shubin2, LI Shixian1   

  1. 1. School of Information Science and Technology, Sun Yat-Sen University, Guangzhou 510275, China
    2. School of Computer Science and Software Engineering, Shenzhen University, Shenzhen, Guangdong 518060, China
  • Online:2012-07-01 Published:2012-07-02

一种UML2的交互的形式化语义

古思山1+,蔡树彬2,李师贤1   

  1. 1. 中山大学 信息科学与技术学院,广州 510275
    2. 深圳大学 计算机与软件学院,广东 深圳 518060

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交互的应用和研究奠定了坚实的理论基础。

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