Semantics and Verification of Data Flow in UML 2.0 Activities

One of the major changes in going from UML 1.5 to UML 2.0 is the reengineering of activity diagrams. This paper examines activity diagramies as described in the current version of the UML 2.0 standard by defining a denotational semantics. It covers basic control flow and data flow, but excludes hierarchy, expansion nodes, and exception handling (see [Störrle, H., Semantics of Control-Flow in UML 2.0 Activities, in: P. Bottoni, C. Hundhausen, S. Levialdi and G. Tortora, editors, Proc. IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC) (2004), pp. 235-242, Störrle, H., Semantics of Exceptions in UML 2.0 Activities (2004), submitted to Journal of Software and Systems Modeling, May, 9th, available at www.pst.informatik.uni-muenchen.de/~stoerrle, Störrle, H., Semantics of Expansion Nodes in UML 2.0 Activities, in: I. Porres, editor, Proc. 2nd Nordic Ws. on UML, Modeling, Methods and Tools (NWUML'04), 2004] for these issues). The paper shows, where the constructs proposed in the standard are not so easily formalized, and how the formalisation may be used for formal analysis.