【摘要】UML活动图是一种特殊的状态机,被认为最适合描述软件过程建模,但其缺乏精确的语义,不利于对模型进行形式化分析和验证。针对传统描述逻辑无法表达动态行为和时序特征的不足,提出了一种基于时态描述逻辑的UML活动图形式化规约方案,讨论了时序描述逻辑时序扩展部分的语法和语义,研究了UML活动图的静态语义和动态语义的ALCQIUS形式化规约,通过具体应用实例说明所提方案的可行性。