This repository contains a collection of microservice relisiency patterns modeled as Continuous-Time Markov Chains (CTMC) using the PRISM probabilistic model checker.
The collection is under development and so far includes CTMC models for the following resiliency patterns:
These two pattern models are described and analyzed in our companion ICSA 2020 paper (link below). The PRISM specification for each model is available in the models folder.
See the PRISM documentation to learn more about the PRISM model and property specification languages.
Please contact us if you have any question or would like to contribute to improve our pattern models catalog.
MENDONÇA, N. C., ADERALDO, C. M., CÁMARA, J., GARLAN, D. "Model-Based Analysis of Microservice Resiliency Patterns." In: IEEE International Conference on Software Architecture (ICSA), 2020, Salvador, Brazil. [PDF]