AbstractThe 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.
Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification; G.3 [Probability and Statistics]
Additional Key Words and Phrases: probability, reliability, action system, refinement
Selected references
- R. J. R. Back and R. Kurki-Suonio. Decentralization of process nets with centralized control. In Proceedings of the Second Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pages 131-142, Montreal, Quebec, Canada, 17-19 August 1983.
- Paul Gardiner and Carroll Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87(1):143-162, 16 September 1991.
- P H B Gardiner and Carroll Morgan. A single complete rule for data refinement. Formal Aspects of Computing, 5(4):367-382, 1993.
- C. A. R. Hoare, Jifeng He, and J. W. Sanders. Prespecification in data refinement. Information Processing Letters, 25(2):71-76, 6 May 1987.
- He Jifeng, K. Seidel, and A. McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28(2-3):171-192, April 1997.
- Carroll Morgan, Annabelle McIver, and Karen Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325-353, May 1996.