The growing importance of big data applications calls for the development of tools and methods to facilitate the development of high-quality applications. In this paper, we propose a model-driven approach for the specification and formal verification of the Hadoop-MapReduce workflow using the de facto standard BPMN2 and the Event B formal method. This approach is automated by the development of a prototype tool called BPMN-MapRed2EventB.

The BPMN2 language suffers from the absence of a precise formal semantics of the various notations used, which often leads to ambiguities. In addition, this language does not have a proof system that validates a BPMN2 specification. Consequently, the use of a formal method, such as Event B, is a solution for dealing with the shortcomings found in the BPMN2 language. We propose in this paper a model-driven approach based on meta-model and meta-model transformation implemented in KerMeta to specify and formally verify workflows.