On Compositional Reasoning for Guaranteeing Probabilistic Properties

TL;DR

This paper introduces a formal framework for probabilistic system analysis, enabling reasoning about failures and reliability guarantees in systems composed of multiple units with probabilistic behaviors.

Contribution

It presents a novel symbolic reasoning approach for probabilistic systems using monad-like constructs, extending previous work with detailed explanations and case studies.

Findings

Derives upper bounds for system failure probabilities

Models component behaviors with monad-like constructs

Provides a comprehensive reasoning framework for probabilistic guarantees

Abstract

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.