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

A Formal Semantics for Interactions in UML2

作　　者：古思山[1] 蔡树彬[2] 李师贤[1] 

机构地区：[1]中山大学信息科学与技术学院,广州510275 [2]深圳大学计算机与软件学院,广东深圳518060

出　　处：《计算机科学与探索》2012年第7期631-643,共13页Journal of Frontiers of Computer Science and Technology

基　　金：广东省自然科学基金No.10351806001000000;广东省高校优秀青年创新人才培养计划项目No.LYM09121;深港创新圈项目No.ZYB200907060012A;深圳市科技计划项目No.JC201005280434A~~

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

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]