On January 28^th Larisa Safina successfully defended her PhD Thesis “Formal methods and patterns for microservices”.

Microservices is an architectural style that organizes an application as a set of highly granular loosely-coupled services. Microservices often use choreography instead of orchestration as a model of coordination. A choreography is a global specification of how endpoints in a concurrent system should communicate. The algorithm of End Point Projection translates a global choreography model to a set of local specifications. The inverse choreography extraction algorithm recreates a global choreography from local specifications.

In her thesis, Safina investigates the microservices architectural style, its quality model and formal approaches to data communication and querying. It provides three main contributions. The first contribution is the comparison of microservices against previous engineering approaches and the analysis of their strong and weak sides, which can be exploited for developing solid architecture patterns. The second is the implementation of the choreography extraction algorithm proposed by Cruz-Filipe et al. and conducting the empirical analysis of its performance. Also, some improvements to the original algorithm were investigated. The third is the development of TQuery, a framework for document-oriented queries, inspired by MQuery, the sound variant of the MongoDB query language. TQuery was implemented as a sub-language inside of the microservices-based programming language Jolie.