MapReduce is a widespread programming paradigm used to develop scalable parallel applications in various fields. Despite the simplicity of the MapReduce model, using it to effectively solve real-life problems can be challenging for developers and designers. Furthermore, ensuring the reliability and correct requirements of any system is fundamental at the early stage of development, as late corrections are estimated to be more than 200 times greater than corrections during requirement engineering. Therefore, a systematic approach is required to assist designers in developing reliable MapReduce applications. In this paper, we present a design pattern-based approach to the specification and formal verification of MapReduce applications using the BPMN notation and the Event B method.