基于进程代数的UML序列图的形式语义  

The Formal Semantics of UML Sequence Diagram Based on Process Algebra

作　　者：李青山[1] 褚华[1] 陈平[1] 

机构地区：[1]西安电子科技大学软件工程研究所,西安710071

出　　处：《计算机科学》2004年第4期173-175,183,共4页Computer Science

基　　金："十五"军事电子预研重点课题项目(项目编号413060601)

摘　　要：UML序列图用于建模实例间动态交互过程.但UML规范并没有给出其形式化的动态语义,这不利于对模型进行形式化验证和证明。本文把序列图中的事件动作及其执行序列映射为进程代数中的进程表达式,利用进程代数语义框架来构建UML序列图的形式语义。首先,建立了序列图到进程代数的语义映射规则;然后用Plotkin风格的结构化操作语义给出并证明条件组合算子演绎规则;最后,归纳定义了算子次序约束条件并证明了其可终止性。UML Sequence diagram models interactions between instances, but UML has no strictly defined formal dynamic semantics. So it is difficult to do formal verification and proof on the models. In this paper,based on the mapping of the actions of sequence diagram to the process expressions of process algebra,a formal semantics of UML sequence diagram is built. First .mapping rules are given between sequence diagram and process algebra,and next a set of Plotkin-stylc structural operational semantics is used to define inductive rules for composition operator of UML sequence diagram process algebra. Finally, we introduce ordering constraints conditions for compositional operator and prove it's property of termination.

关 键 词：面向对象 建模语言 UML 进程代数 序列图 形式语义 

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