{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,21]],"date-time":"2023-06-21T04:14:41Z","timestamp":1687320881104},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2023,3,6]],"date-time":"2023-03-06T00:00:00Z","timestamp":1678060800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"Partial synchrony is a model of computation in many distributed algorithms\nand modern blockchains. These algorithms are typically parameterized in the\nnumber of participants, and their correctness requires the existence of bounds\non message delays and on the relative speed of processes after reaching Global\nStabilization Time. These characteristics make partially synchronous algorithms\nparameterized in the number of processes, and parametric in time bounds, which\nrender automated verification of partially synchronous algorithms challenging.\nIn this paper, we present a case study on formal verification of both safety\nand liveness of the Chandra and Toueg failure detector that is based on partial\nsynchrony. To this end, we first introduce and formalize the class of symmetric\npoint-to-point algorithms that contains the failure detector. Second, we show\nthat these symmetric point-to-point algorithms have a cutoff, and the cutoff\nresults hold in three models of computation: synchrony, asynchrony, and partial\nsynchrony. As a result, one can verify them by model checking small instances,\nbut the verification problem stays parametric in time. Next, we specify the\nfailure detector and the partial synchrony assumptions in three frameworks:\nTLA+, IVy, and counter automata. Importantly, we tune our modeling to use the\nstrength of each method: (1) We are using counters to encode message buffers\nwith counter automata, (2) we are using first-order relations to encode message\nbuffers in IVy, and (3) we are using both approaches in TLA+. By running the\ntools for TLA+ and counter automata, we demonstrate safety for fixed time\nbounds. By running IVy, we prove safety for arbitrary time bounds. Moreover, we\nshow how to verify liveness of the failure detector by reducing the\nverification problem to safety verification. Thus, both properties are verified\nby developing inductive invariants with IVy.<\/jats:p>","DOI":"10.46298\/lmcs-19(1:17)2023","type":"journal-article","created":{"date-parts":[[2023,3,6]],"date-time":"2023-03-06T09:55:18Z","timestamp":1678096518000},"source":"Crossref","is-referenced-by-count":0,"title":["A case study on parametric verification of failure detectors"],"prefix":"10.46298","volume":"Volume 19, Issue 1","author":[{"given":"Thanh-Hai","family":"Tran","sequence":"first","affiliation":[]},{"given":"Igor","family":"Konnov","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2023,3,6]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/11031\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/11031\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:20:38Z","timestamp":1687292438000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/8860"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,6]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-19(1:17)2023","relation":{"has-preprint":[{"id-type":"arxiv","id":"2112.08826v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2112.08826v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2112.08826","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2112.08826","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,6]]}}}