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

摘要：

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

关键词：UML序列图、形式语义、进程代数、组合算子、结构化操作语义

所属期刊栏目：31

分类号：TP3(计算技术、计算机技术)

资助基金：信息产业部电子科学院军事电子预研项目413060601

在线出版日期：2004-06-11（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：173-175,183