A Temporal Logic Semantics for UML Activity Diagrams

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.