UML_AD2EventB: An Approach to Generating Event B Specification from UML Activity Diagrams for the Workflows Specification and Verification

In this paper, we present a new approach to generating Event B specification from UML Activity Diagrams (AD). The goal of this work is to define a formal semantics of activity diagrams that is suitable for workflows modelling. The semantics should allow verification of functional requirements using the B powerful support tools like B4free. In important characteristic of workflows is that the workflow systems are reactive systems. In this paper, we present a formal syntax and semantic for UML AD endowed with interactive aspects (send/receive event concepts), and we illustrate the proposed technique by an example of workflow application.