  We present a framework to formally describe probabilistic system behavior and
symbolically reason about it. In particular we aim at reasoning about possible
failures and fault tolerance. 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 most suited 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 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
and their evolvement over system runs. This serves as basis for deriving
probabilities of events, in particular failure probabilities. The work
presented in this paper slightly extends a complete framework and a case study
which has been previously published. One focus of this report is a more
detailed explanation of definitions and a more comprehensive description of
examples.
