| Title |
„Redis Cluster“ podėlio sistemos tyrimas, taikant formalius metodus / |
| Translation of Title |
Analysis of the "redis cluster" cache system using formal methods. |
| Authors |
Kontrimas, Mantas |
| Full Text |
|
| Pages |
123 |
| Abstract [eng] |
This master thesis analyzes the correctness of the popular cache system “Redis Cluster”. The system is investigated using formal methods – in the TLA+ language two formal specifications of the system are formulated: the abstract and detailed specifications. The abstract specification models system requirements and the more detailed specification is at the code abstraction level and models actual system algorithm and behavior. Using model checker it was checked if the system holds the property that only one master and its slaves must be responsible for the hash slot. The model checking showed that there are situations when the analyzed property is not satisfied and the system works incorrectly. Found issues were reproduced at the actual system and the ways how to fix these problems were proposed. |
| Dissertation Institution |
Vilniaus universitetas. |
| Type |
Master thesis |
| Language |
Lithuanian |
| Publication date |
2021 |
