{"content":[{"text":"Veriﬁcation and Visualization of a Consensus \n Algorithm using TLA+","bbox":{"left":0.193057,"top":0.215379,"width":0.611131,"height":0.057537000000000005}},{"text":"Afonso das Neves Fernandes \n Faculty of Sciences, University of Porto","bbox":{"left":0.300484,"top":0.297614,"width":0.396185,"height":0.040775000000000006}},{"text":"Rolando da Silva Martins \n Faculty of Sciences, University of Porto","bbox":{"left":0.300484,"top":0.351767,"width":0.396185,"height":0.04077399999999998}},{"text":"July 1, 2021","bbox":{"left":0.437525,"top":0.40982,"width":0.12213000000000002,"height":0.01813199999999998}},{"text":"In our work, we used TLA+ to formalize the consensus algorithm used in \n Ceph (which is based on Paxos). We found that the formalization was useful \n to clarify how the algorithm works and to prove its correctness. The speciﬁca- \n tion can be found at: https://github.com/afonsonf/ceph-consensus-spec.","bbox":{"left":0.181134,"top":0.467143,"width":0.654709,"height":0.071546}},{"text":"We also found that the speciﬁcation could catch real world bugs of the \n algorithm. To do this we introduced a bug that was previously present in \n the algorithm and then evaluate if the model checker would catch it, which \n was found to be successful.","bbox":{"left":0.181134,"top":0.560045,"width":0.6349349999999999,"height":0.06982999999999995}},{"text":"During the formalization of the algorithm, we developed a visualiza- \n tion tool to help understand the algorithm, its bugs, and how the spec- \n iﬁcation could be improved to make it more eﬃcient. The tool accepts \n for the visualization both state graphs in the dot format and error traces \n from TLC. The tool can be found at: https://github.com/afonsonf/ \n tlaplus-graph-explorer.","bbox":{"left":0.181134,"top":0.651243,"width":0.635083,"height":0.10632299999999995}},{"text":"We propose to present our ﬁndings on formalizing the algorithm and \n using the visualization tool. This proposal follows the work done by Afonso \n Fernandes in his Master thesis (still not published).","bbox":{"left":0.181134,"top":0.778921,"width":0.634954,"height":0.051590000000000025}},{"text":"1","bbox":{"left":0.493789,"top":0.875215,"width":0.00955199999999995,"height":0.015109999999999957}}],"images_bbox":[],"images_bbox_not_text_overlap":[]}