Moritz Systems are experts in embedded solutions that host innovative solutions in Fintech, Insurtech, Smart Energy, Smart Buildings. Industry 4.0 (IIoT), HealthTech, Medtech, Digital Health, Martech, Sustainability and Waste Management.
Continuing from our previous article, let us take an example of how to write a TLA+ proof for a real-world specification of a distributed system. For this exercise we will go through the Voucher Trading System process as specified by the RFC3506 hosted by IETF. The distributed and concurrent systems require a consensus protocol to achieve overall system reliability and immunity to failures of nodes. We decided to select for this VTS network a simple Two-phase commit protocol.