CoreDump: IoT Consensus Algos and PML
Welcome to CoreDump, the One Stop for Techies!
In this episode we continue with PML examples with TLA+ formal specs for consensus and fault tolerance design patterns, we introduce an example from GitHub, a one-step byzantine consensus algo, for IoT sensor fusion, maybe you can write it in RavaTTT actions?
Dump 01.10.2022.09.18.AM
Gecko: Statefulness is ever rampant in TLA+, here is a cheat sheet….
Summary of TLA+ — Microsoft Azure
To summarize, we PML the state machines with time domain scheduling of actions, synchronous or asynchronous with a set or tuple-based data structure framework with action operators.
In short apart from provable class diagrams, we have state diagrams….
Lisa: Sounds simple, and the design patterns are straight forward?
Gecko: Yes, the best practices are simple, and, in this episode, we consider some fault tolerant designs!
Here is a State Diagram Cartoon…
We have two start states, V0 for a data of 0 and V1 for a data of 1, and two end states, U0 for a consensus of 0 and U1 for a consensus of 1. And the states D0 and D1 and S0 and S1.
And the Classes…..
You can review the code here, The code:
It should be fairly approachable now…
Lisa: I get really close to the code now, right in it….