Abstract: Converting the UML chart into the formal specification is an effective way to achieve more precise semantics and expand the application scope of formal software methods. In view of the strong decidable reasoning ability of Description Logics(DLs), the formalization of UML state chart based on Temporal Description Logics(TDLs) is proposed. The temporal operators are applied to extend the basic description logics, and then get the formal specificationTDLs, which can express the dynamic and temporal semantics. The general mapping rules that state how a state chart is transformed into a TDLs specification are given. The example shows that the method formalizing the UML state chart based on TDLs is feasible.

Key words: Description Logics(DLs), temporal extension, Temporal Description Logics(TDLs), state chart, formalization

摘要： 将UML图形转换成形式化规范是一种精确UML语义、扩大形式化软件方法适用范围的有效途径。鉴于描述逻辑强的可判定推理能力，提出一种采用时序描述逻辑形式化UML状态图，对描述逻辑进行时序扩展，得到可以表示动态和时序语义的形式化规范——时序描述逻辑，给出一套UML状态图向时序描述逻辑表达式转换的规则，通过实例验证了该方法的可行性。

关键词: 描述逻辑, 时序扩展, 时序描述逻辑, 状态图, 形式化

CLC Number: 

• N945