作者：李青山; 褚华; 陈平面向对象建模语言uml进程代数序列图形式语义
摘要：UML序列图用于建模实例间动态交互过程,但UML规范并没有给出其形式化的动态语义,这不利于对模型进行形式化验证和证明.本文把序列图中的事件动作及其执行序列映射为进程代数中的进程表达式,利用进程代数语义框架来构建UML序列图的形式语义.首先,建立了序列图到进程代数的语义映射规则;然后用Plotkin风格的结构化操作语义给出并证明务件组合算子演绎规则;最后,归纳定义了算子次序约束条件并证明了其可终止性.
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
