The Formal Semantics of UML Sequence Diagram Based on Process Algebra
基于进程代数的UML序列图的形式语义

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.