Reliability assessment through probabilistic refinement

Abstract

The paper presents an approach to reasoning about probabilistic systems that are to be implemented in a parallel or distributed manner. The approach allows us to obtain a quantitative assessment of the reliability of a system under construction. We base our reasoning on the application of refinement and in particularly data refinement techniques to the specification of systems containing a level of overall system reliability. Performing refinement of such a probabilistic specification we not only ensure the correctness of the system design but also establish a quantitative link between the overall system reliability and reliabilities of components from which the system is to be implemented. We illustrate the approach by designing a system that models data transmission over an unreliable medium.