On Compositional Reasoning for Guaranteeing Probabilistic Properties Jan Olaf Blech

Abstract. We present a framework to formally describe probabilistic system be-havior 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 com-ponents is modeled using monad like constructs that serve as an abstract repre-sentation for system behavior. We introduce rules to reason about these represen-tations 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 evolve-ment 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 [4]. One focus of this report is a more detailed explanation of definitions and a more comprehensive description of examples.