João Quelhas Guterres Serrão Fitas
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