Probabilistic compositional reasoning for guaranteeing fault tolerance properties

We present a framework to formally describe system behavior and symbolically reason about possible failures. We regard systems which are composed of different units: sensors, computational parts and actuators. Considering worst-case failure behavior of system components, our framework is used to derive reliability guarantees for composed systems. The behavior of system components is modeled using monad like constructs that serve as an abstract representation for system behavior. We introduce rules to reason about these representations and derive results like, e.g., guaranteed upper bounds for system failure. Our approach is characterized by the fact that we do not just map a certain component to a failure probability, but regard distributions of error behavior. These serve as basis for deriving failure probabilities