• Formally Documenting Tenderbak...

Treffer: Formally Documenting Tenderbake

Title:
Formally Documenting Tenderbake
Authors:
Conchon, Sylvain, Korneva, Alexandrina, Bozman, Çagdas, Iguernlala, Mohamed, Mebsout, Alain
Contributors:
Nomadic Labs, Université Paris-Saclay, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Functori, ANR-16-CE25-0006,PARDI,Vérification de systèmes distribués paramétrés(2016)
Source:
Open Access Series in Informatics, In press, ⟨10.4230/OASIcs.FMBC.2021.5⟩
Publisher Information:
CCSD; Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.
Publication Year:
2021
Collection:
collection:CNRS
collection:ENS-CACHAN
collection:CENTRALESUPELEC
collection:UNIV-PARIS-SACLAY
collection:TEST-HALCNRS
collection:UNIVERSITE-PARIS-SACLAY
collection:ANR
collection:ENS-PARIS-SACLAY
collection:ENS-PSACLAY
collection:GS-COMPUTER-SCIENCE
collection:LMF
collection:LMF-PP
collection:LMF-CDS
Subject Terms:
ACM: D.: Software, D.2: SOFTWARE ENGINEERING, D.2.4: Software, Program Verification, D.2.4.3: Formal methods, [INFO.INFO-LO]Computer Science [cs], Logic in Computer Science [cs.LO]
Original Identifier:
HAL: hal-03398884
Document Type:
Zeitschrift article<br />Journal articles
Language:
English
ISSN:
2190-6807
Relation:
info:eu-repo/semantics/altIdentifier/doi/10.4230/OASIcs.FMBC.2021.5
DOI:
10.4230/OASIcs.FMBC.2021.5
Access URL:
https://hal.science/hal-03398884
https://hal.science/hal-03398884v1/document
https://hal.science/hal-03398884v1/file/main.pdf
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.03398884v1
Database:
HAL

Weitere Informationen

In this paper, we propose a formal documentation of Tenderbake, the new Tezos consensus algorithm, slated to replace the current Emmy family algorithms. The algorithm is broken down to its essentials and represented as an automaton. The automaton models the various aspects of the algorithm: (i) the individual participant, referred to as a baker, (ii) how bakers communicate over the network (the mempool) and (iii) the overall network the bakers operate in. We also present a TLA+ implementation, which has proven to be useful for reasoning about this automaton and refining our documentation. The main goal of this work is to serve as a formal foundation for extracting intricate test scenarios and verifying invariants that Tenderbake's implementation should satisfy.