Towards the Formal Analysis of UML Activity Diagrams in a Calculus of Context-aware Ambients

The Unified Modeling Language (UML) is the industrial de-facto standard for designing systems. It has been used widely in many industrial applications. However, the lack of formal semantics for UML makes it unsuitable for formal verification. As such, UML is limited when it comes to the design of safety/security critical systems where faults can cause damages to people, properties, or the environment. This paper proposes an attempt to define a formal semantics for the UML activity diagrams. An algorithm is proposed that translates an activity diagram into a process in a Calculus of Context-aware Ambients (CCA). This process can then be formally analysed using the tool support for CCA. Hence, errors can be detected and fixed early during the system development life-cycle. The pragmatics of the proposed approach is demonstrated using a case study in e-commerce.