摘要： UML序列图用于建模实例间动态交互过程．但UML规范并没有给出其形式化的动态语义，这不利于对模型进行形式化验证和证明。本文把序列图中的事件动作及其执行序列映射为进程代数中的进程表达式，利用进程代数语义框架来构建UML序列图的形式语义。首先，建立了序列图到进程代数的语义映射规则；然后用Plotkin风格的结构化操作语义给出并证明务件组合算子演绎规则；最后，归纳定义了算子次序约束条件并证明了其可终止性。

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