UML activity diagrams, the reputed best application to the description of the software process modeling. Is a special state machine. However, it is not suitable for the analysis and verification of the model due to its deficiency of exact semantics. In the light of the insufficiency for the manifestation of the dynamic behavior and the temporal feature of traditional description logic, a program of formal specification of UML activity diagram based on temporal description logic was put forward in the paper with syntax and semantics of the temporal extension of the temporal description logic being discussed and the ALCQIUS formal specifications of the static semantics and the dynamic semantics of the UML activity diagram also being studied. Finally, the feasibility of the program was proved by the specific applied examples.%UML活动图是一种特殊的状态机,被认为最适合描述软件过程建模,但其缺乏精确的语义,不利于对模型进行形式化分析和验证.针对传统描述逻辑无法表达动态行为和时序特征的不足,提出了一种基于时态描述逻辑的UML活动图形式化规约方案,讨论了时序描述逻辑时序扩展部分的语法和语义,研究了UML活动图的静态语义和动态语义的ALCQIUS形式化规约,通过具体应用实例说明所提方案的可行性.
展开▼
