FaultRay: Why We Formalized Cascade Failure Propagation as a Labeled Transition System

Gremlin, Steadybit, and AWS FIS act on running systems, but they do not answer an architecture’s availability ceiling.

Fault Tree Analysis and Reliability Block Diagrams can answer that analytically, but they depend on static trees and independence assumptions.

In cloud infrastructure, shared-underlay failures can hit database, cache, and application tiers together, and RBDs can overestimate availability.

FaultRay is a research prototype for correlated failure propagation without production touch; it formalizes cascade propagation as a labeled transition system over a dependency graph.

CPS state is S=(H,L,T,V): health can only worsen during a run, and the implementation and formal spec are in the listed src and docs files.