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