João Quelhas Guterres Serrão Fitas

Co-advisor: A. Rito Silva


Detection of Invariant Violations in Microservices


Tese submetida para provas de mestrado em Engenharia Informática e de Computadores Instituto Superior Técnico, Universidade de Lisboa.

Abstract

In a monolith, functionalities are executed as transactions, that are isolated from each other. In a mi- croservice architecture, functionalities may be composed of multiple transactions, each executed in a different microservice. When functionalities execute concurrently, these individual transactions may in- terleave, generating states that violate correctness invariants. This work studies techniques to: 1) detect automatically executions that may cause invariants to be violated, and 2) automatically present concrete executions that illustrate those violations. We have built a tool, named DAVIAC, that achieves these goals. The tool encodes the application code and the invariants as Satisfiability Modulo Theories formu- las and then uses a Satisfiability Modulo Theories solver to explore the space of possible interleavings and input parameters. When the violation of an invariant is found, the tool captures the exact inter- leaving that causes the violation. We have evaluated the tool by applying it to different microservice applications.

Publicações

Detection of Invariant Violations in Microservices
João Quelhas Guterres Serrão Fitas
MSc Thesis. Instituto Superior Técnico, Universidade de Lisboa.
November 2024.
Available BibTeX, MSC Thesis, and extended abstract, and mid-term report.
Deteção de Violação de Invariantes em Microserviços.
J. Fitas, R. Soares, A. Silva and L. Rodrigues.
Actas do décimo quinto Simpósio de Informática (Inforum), Lisboa, Portugal, Sep. 2024.
Available BibTeX, extended report (pdf).

Luís Rodrigues