Monitor and Update Master Data Case Studies

Model decomposition is a powerful tool to scale the design of large and complex systems. It enables developers to separate components development from the concerns of their integration and orchestration. Event-B is a stepwise refinement based formal method, which also includes decomposition within its scope. Currently, there exists three different styles of decomposition for Event-B. This paper gives some useful insights and proposes some modelling guidelines for effectively applying these Event-B decomposition techniques. We illustrate our approach through several case studies