摘要

UML活动图可以表示不同抽象级的控制流,很适合用于对系统的行为建模.但是缺乏精确的语义使得难以对它所表示的系统行为进行分析.XYZE是一可执行线性时序逻辑语言,既可描述系统的动态行为又可表示程序性质,用它对活动图形式化后,就可在统一的逻辑框架下分析活动图的性质.定义了一个有向图结构用以表示UML活动图,再给出其XYZE语义,并用一个例子说明活动图到XYZE的语义转换,为进一步的分析提供形式化基础.