Enhancing Formal Semantics of Activity Diagram with Object Nodes

UML Activity Diagram has been widely used by practitioners to model dynamic aspects of any real world system. But UML is not based on firm mathematical semantics therefore it is unable to be checked for presence of errors. The latest version of UML released by Object Management Group (OMG) in 2015 still lacks standard formal semantics. Our earlier publication presented formalization of structural semantics of UML 2.5 Activity Diagram in Z notation. This paper is an extension of our previous work by comprehensive formalization of Object Node. Amongst the three basic nodes offered by Activity Diagram, an Object Node is uniquely characterized to carry object tokens from source to destination. An Object Node can hold a fixed number of tokens at a particular time hence maintaining a particular state. The Object Management Group (OMG) defined structural semantics of Object Nodes along with its successors like Data Store Node, Central Buffer Node and Activity Parameter Node have been formalized in Z notation. Finally the formal semantics have been checked and verified using various proof techniques offered by Z/EVES toolkit.