UML活动图的时序逻辑语义

A Temporal Logic Semantics for UML Activity Diagrams

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

Abstract UML activity diagrams can be used to describe the control flow of different abstract levels and are very suitable for modeling system behaviors. However, the lack of precise semantics makes it difficult to analyze properties of the system they describe. In this paper, a variant of UML activity diagrams-XYZ activity diagrams which can be translated easily from activity diagrams is given, and a data structure of directed graph used to represent the activity diagram is defined. Its semantics then is interpreted using the executable linear temporal logic language XYZ/E, which can represent both dynamic semantics and static semantics. Compared with other formalizations such as CSP, ASM, and FSP, the XYZ/E semantics for UML activity diagrams is more intuitive. And the formalized activity diagram can be analyzed within a unified logical framework. An example is included.