-
Tenderbake -- A Solution to Dynamic Repeated Consensus for Blockchains
Authors:
Lăcrămioara Aştefanoaei,
Pierre Chambart,
Antonella Del Pozzo,
Thibault Rieutord,
Sara Tucci,
Eugen Zălinescu
Abstract:
First-generation blockchains provide probabilistic finality: a block can be revoked, albeit the probability decreases as the block sinks deeper into the chain. Recent proposals revisited committee-based BFT consensus to provide deterministic finality: as soon as a block is validated, it is never revoked. A distinguishing characteristic of these second-generation blockchains over classical BFT prot…
▽ More
First-generation blockchains provide probabilistic finality: a block can be revoked, albeit the probability decreases as the block sinks deeper into the chain. Recent proposals revisited committee-based BFT consensus to provide deterministic finality: as soon as a block is validated, it is never revoked. A distinguishing characteristic of these second-generation blockchains over classical BFT protocols is that committees change over time as the participation and the blockchain state evolve. In this paper, we push forward in this direction by proposing a formalization of the Dynamic Repeated Consensus problem and by providing generic procedures to solve it in the context of blockchains. Our approach is modular in that one can plug in different synchronizers and single-shot consensus instances. To offer a complete solution, we provide a concrete instantiation, called Tenderbake, and present a blockchain synchronizer and a single-shot consensus algorithm, working in a Byzantine and partially synchronous system model with eventually synchronous clocks. In contrast to recent proposals, our methodology is driven by the need to bound the message buffers. This is essential in preventing spamming and run-time memory errors. Moreover, Tenderbake processes can synchronize with each other without exchanging messages, leveraging instead the information stored in the blockchain.
△ Less
Submitted 25 February, 2021; v1 submitted 31 January, 2020;
originally announced January 2020.
-
Compositional Verification for Timed Systems Based on Automatic Invariant Generation
Authors:
Lacramioara Astefanoaei,
Souha Ben Rayana,
Saddek Bensalem,
Marius Bozga,
Jacques Combaz
Abstract:
We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automatically generate new invariants which capture the constraints i…
▽ More
We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automatically generate new invariants which capture the constraints induced by the synchronisations between components. The method has been implemented in the RTD-Finder tool and successfully experimented on several benchmarks.
△ Less
Submitted 16 September, 2015; v1 submitted 16 June, 2015;
originally announced June 2015.
-
Timed Orchestration for Component-based Systems
Authors:
Chih-Hong Cheng,
Lacramioara Astefanoaei,
Harald Ruess,
Souha Ben Rayana,
Saddek Bensalem
Abstract:
Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We forma…
▽ More
Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We formalize this problem of configuring and orchestrating flexible production lines as a parameter synthesis problem for systems of parametric timed automata, where interactions are based on skills. Parameter synthesis problems for interaction-level LTL properties are translated to parameter synthesis problems for state-based safety properties. For safety properties, synthesis problems are solved by checking satisfiability of $\exists\forall$SMT constraints. For constraint generation, we provide a set of computationally cheap over-approximations of the set of reachable states, together with fence constructions as sufficient conditions for safety formulas. We demonstrate the feasibility of our approach by solving typical machine configuration problems as encountered in industrial automation.
△ Less
Submitted 20 May, 2016; v1 submitted 21 April, 2015;
originally announced April 2015.
