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….