Using UML Activity Diagrams and Event B for Distributed and Parallel Applications

This paper presents a specification and verification technique for distributed and parallel applications using formal and semi-formal methods. The proposed technique uses UML and Event B. The design is initially expressed graphically with UML, then translated into Event B and verified using the B powerful support tools. In this paper, we focus on the translation of activity diagrams into Event B, in order to verify workflow properties of distributed and parallel applications with the B prover. We present translation rules of activity diagrams into Event B, and relation between hierarchical decomposition of activities in UML activity diagrams and the refinement in Event B.