Towards Formalizing Microservices Architectural Patterns with Event-B

Microservices have recently emerged as an architectural style in which applications are composed of small services, each running on its own process and communicating with others using lightweight mechanisms. In order to guide the construction of such applications, microservices architectural patterns have been proposed to document knowledge and address recurring situations. However, these patterns are mostly described in an informal way which may lead to ambiguity as well as to their incorrect usage. This paper proposes a formal approach to deal with these issues by formalizing microservices architectural patterns with the Event-B modeling language. The approach aims to provide formal models of these patterns and related results (e.g. formal proofs, visualizations), with the goal of contributing not only to their precise comprehension but also to the development of correct-by-construction microservices applications.