统一建模语言(UML)是在多种面向对象建模方法联合的基础上形成的建模语言。它以支持面向对象、可视化建模和强大的表达能力等优点已经被人们广泛的用于多种类型的系统建模。然而, UML是半形式化的——其语法结构采用了形式化的规约,但其语义部分则是用非形式化的自然语言来描述。为了解决UML半形式化的缺点,学者们提出对其形式化,以达到精确的目的。描述逻辑(Description Logics, DLs)是知识表示的一种形式化语言,是一阶逻辑的一个可决定的子集,具有很强的表达能力;它将推理作为中心服务,注重关键推理服务的可判定性即它能保证推理算法总能停止,并返回正确的结果。本论文拟用描述来形式化UML2.0顺序图,描述逻辑是一个逻辑序列,其最基本的描述逻辑是ALC,通过向其添加构造子,可以得到不同表达能力的描述逻辑;根据表示目的的不同可以选择具有相应表达能力的描述逻辑。本文的工作主要分为两部分。(1)描述逻辑的动态和时序扩展。描述逻辑能够精确的描述UML顺序图的静态部分;为了使描述逻辑能对动态和时态领域进行精确的描述,通过选定描述逻辑适中的描述逻辑中加入动态维度和时序算子,对其进行动态和时态扩展;其次对扩展后描述逻辑的Tableau算法的判定性(Termination)、可靠性(Soundness)和完备性(Completeness)进行探讨。(2)扩展后的描述逻辑到UML顺序图的转换规则。利用UML2.0顺序图新增的交互片段操作符将UML2.0顺序图划分为多个片段;再利用上部分扩展后的描述逻辑分别对UML2.0顺序图的片段和交互操作符分别进行形式化描述以达到形式化UML2.0顺序图的目的。通过利用描述逻辑对UML2.0顺序图进行形式化,使UML2.0顺序图的语义能够精确的描述,从而解决了其因语义不精确性而在建模时产生的一些不一致等错误的缺点。