From UML Activity Diagrams to Event B for the Specification and the Verification of Workflow Applications

This paper presents a new event-B based approach to reasoning about workflow applications. We show how an event-B model can be structured from UML Activity diagrams (UML AD) and then used to give a formal semantic to UML AD which supports proofs of their correctness. More precisely, we give rules for the translation of UML AD into event-B language. In particular, we propose a solution that uses the refinement in Event B to encode the hierarchical decomposition of activities in UML AD. The event-B method allows the definition of invariant describing required properties (deadlock-inexistence, liveness, fairness) and provides an automatic proof. We discuss the contributions and by an example of a workflow application, we illustrate the proposed approach.