A Survey on Event-B Decomposition

Abstract

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 refinementbased formal method, equipped with three decomposition styles that come with solid semantic foundations and strong tool support. This paper intends to give some useful insights and modelling guidelines for using these decomposition styles, illustrated by an actual development of a master data updating system.