Design Verification
-
Tutorials
- Quick Start: Modeling and Validating Distributed Systems in FizzBee
- Getting Started
- Guard Clauses And Enabling Conditions
- Config and Front Matter
- Liveness and Fairness
- Enums, Records, and Collections
- Modeling msg delivery guarantees
- Actors / Roles
- Channels
- Implicit Fault Injection
- Symmetry Reduction
- Probabilistic Modeling
- Performance Modeling
- Whiteboard Visualizations
- Current Limitations
-
Examples
- Cycle Detection in Linked List
- Die Hard
- EWD426 Token Ring
- Two Phase Commit
- Two Phase Commit (Procedural)
- Two Phase Commit (Actor model/Object oriented)
- Raft Consensus Protocol
- Raft Consensus Protocol - FizzBee Specification for Reasoning
- Knuth-Yao Sampling Algorithm for Random Variate Generation
- Time oblivious Sampling Algorithm for Random Variate Generation
-
Distributed Systems Patterns
- Mutex Pattern
- Read-Write Lock Pattern
- Distributed Lock Pattern
- Optimistic Locking Pattern
- Saga Pattern
- Snapshot Isolation Pattern
- Leader Election (Simplified Raft)
- Compare-And-Swap Pattern
- Producer-Consumer Pattern
- Message Queue Pattern
- Cache Coherence Pattern
- Eventual Consistency Pattern
- Idempotent Operations Pattern
- Circuit Breaker Pattern
- Rate Limiting Pattern
- Write-Ahead Log Pattern
- Event Sourcing Pattern