Formalizing Microservices Patterns with Event-B: The Case of Service Registry

Microservices have emerged as an architectural style in which applications are composed of small and focused services. Several patterns have been proposed to guide the construction of microservices applications. However, they are usually stated in natural-language, which may lead to ambiguity and erroneous application. This paper addresses these issues by advancing in the formalization of microservices patterns using the Event-B method. An Event-B model for the Service Registry pattern is proposed, which is then leveraged for verification/validation purposes. The overall goal is to contribute to the comprehension of microservices patterns and the quality of microservices applications.