@InProceedings{2020:ICSA:Microservices,
      AUTHOR = {Mendon\c{c}a, Nabor C. and Aderaldo, Carlos and C\'{a}mara, Javier and Garlan, David},
      TITLE = {Model-Based Analysis of Microservice Resiliency Patterns},
      YEAR = {2020},
      MONTH = {16-20 March},
      BOOKTITLE = {Proceedings of the 2020 IEEE International Conference on Software Architecture},
      PDF = {http://acme.able.cs.cmu.edu/pubs/uploads/pdf/PID63707632020_ICSA_Microservices.pdf},
      ABSTRACT = {Microservice application developers try to mitigate the impact of partial outages typically by implementing service-to-service interactions that use well-known resiliency patterns, such as Retry, Fail Fast, and Circuit Breaker. However, those resiliency patterns–as well as their available open-source implementations–are often documented informally, leaving it up to application developers to figure out when and how to use those patterns in the context of a particular microservice application. In this paper, we take a first step towards improving on this situation by introducing a model checking-based approach in which we use the PRISM probabilistic model checker to analyze the behavior of the Retry and Circuit Breaker resiliency patterns as continuous-time Markov chains (CTMC). This approach has enabled us to quantify the impact of applying each resiliency pattern on multiple quality attributes, as well as to determine how to best tune their parameters to deal with varying service availability conditions, in the context of a simple client-service interaction scenario.},
      KEYWORDS = {Model Checking, Software Architecture}
}