Modeling and Verifying Microservice Interaction Patterns: From Bach to mCRL2

Défense de mémoire de Corentin Reuther

Amazon, Netix, and Spotify are just a few well-known examples of companies that have widely adopted microservices. For nearly a decade, this architecture has become ubiquitous in most modern IT systems. It's
safe to say that this paradigm shift has profoundly transformed the way we design our systems. Indeed, we've moved from traditional monolithic systems, consisting of a single large software block, to distributed sets of
small, autonomous software components, capable of communicating with each other to ensure the overall smooth running of the system.

There's no denying that these architectures have proven to be very useful. Among the commonly cited benets, we can mention: faster deployment, easier system scalability, and great technological freedom. However,
microservices also introduce new challenges that were absent from monolithic architectures, particularly when it comes to coordinating the entire system and verifying that everything is working as expected.
One way to approach this coordination problem is through abstraction: such a system can be viewed as a set of relatively autonomous software programs, exchanging messages to cooperate. This idea is further
elaborated by Gelernter and Carriero, who propose separating systems into two distinct fundamental concerns: computation and coordination. This distinction allows one to abstract away computational details to reason
more eciently about interaction mechanisms.

With this in mind, this thesis explores the use of the Bach coordination language to model three fundamental interaction mechanisms of microservice architectures: the load balancer, the circuit breaker, and the message
broker. Each mechanism is modeled in Bach and then veried using logical formulas. To extend the scope of this verication, theoretical translation rules into the mCRL2 language are dened, allowing the use of advanced
model-checking tools.

Keywords: microservices, coordination, Bach, Anemone, mCRL2, formal modeling, verication, distributed systems

Contact : Isabelle Daelman - isabelle.daelman@unamur.be
Télecharger : vCal