冉 婕,谢树云,漆丽娟

(云南昭通学院 物理与信息工程学院,昭通 657000)

引言

统一建模语言(Unified Modeling Language,UML)[1,2]是OMG(Object Management Group)提出的标准对象建模语言,又称标准建模语言,是支持模型化和软件系统开发的图形化语言,而且它从不同的角度表达软件设计中的动态和静态信息,但UML是一种半形式化的语言,缺乏精确的语义,不能对系统的交互行为进行形式化分析及论证[3].多数的UML建模工具不能提供完善的管理框架,UML模型的形式化是一个亟待解决的问题.

描述逻辑[4](Decription Logic,DL)是基于概念和角色(即类和属性)的知识表示形式,是对概念化知识进行表示和推理的逻辑形式.传统的DL能描述静态结构知识,但不能表述动态的时序特征,将描述逻辑用时序算子对其进行扩展,可得到表示动态和时序语义的时序描述逻辑.

UML顺序图描述对象间的动态交互能力,体现对象间消息传递的时序特征,将时序描述逻辑应用于UML顺序图,为UML顺序图的形式化提供了更好的研究方法.不同学者研究了顺序图的多种形式化方法,文献[5]给出了一种五元组SD=＜Obj,Msg,Loc,Evn,F>的顺序图的形式化定义及推理过程;文献[6]给出了UML顺序图的一种符合BNF范式的形式化方法,并提出将顺序图转化为Petri网模型的方法;文献[7]给出了UML顺序图的形式化定义并从队列的角度进行了其特性分析;文献[8]对UML2.0顺序图的最大顺序片段形式化,并应用交互操作符得到了顺序图的时序描述逻辑语义.本文在文献[8]的基础上增加了选择交互和循环操作符并……