|
To provide a formalism in which the successful aspects of formal methods (the mathematical specification and rigorous development of an implementation whose functional correctness is assured) can be used --- or extended --- to describe systems exhibiting probabilistic behaviour. To provide a theoretical basis for that formalism which is mathematically sound and elegant yet also supports a usable development method. To transfer the method into practice by using it on realistic systems, for example communications protocols and probabilistic algorithms, to develop current and perhaps new implementations. To exploit features of the method for example by investigating alternatives to the usual probabilistic tolerances. Progress:Building on the thesis work of Claire Jones (Probabilistic Non-determinism, Edinburgh, 1990) we have developed two semantic models. The first extends the weakest precondition formalism of Dijkstra for sequential programs and so is appropriate for reasoning about sequential programs which include an element of probabilistic choice (Probabilistic predicate transformers, Carroll Morgan, Annabelle McIver, Karen Seidel and J.W. Sanders, technical report PRG-TR-4-95, Oxford University Computing Laboratory, 1995, submitted to TOPLAS). The second provides a formalism in which to reason about communicating processes evolving in parallel (Refinement-oriented probability for CSP, Carroll Morgan, Annabelle McIver, Karen Seidel and J.W. Sanders, technical report PRG-TR-12-94, Oxford University Computing Laboratory, 1994, submitted to Formal Aspects of Computing). Both models have been demonstrated on small examples, only, so far: the sequential theory on benchmark simplified random algorithms; the parallel theory on a simplified communications protocol whose channel contaminates its data with certain probability. The sequential theory, which extends Jones work to non determinism (important since it arises from hiding variables, a device essential for spanning levels of abstraction) has been related to the binary-relation model of sequential programs (Probabilistic models for the guarded command language, He Jifeng, Annable McIver and Karen Seidel, in draft, February 1995 ). Healthiness conditions (corresponding to Dijkstras strictness, monotonicity, conjunctivity and continuity) have been discovered which characterise the set of probabilistic programs within the space of probabilistic predicate transformers. Furthermore deterministic probabilistic programs have been characterised (Probabilistic determinism, in preparation). The probabilistic theory of concurrency has been shown to respect a range of models for communicating sequential processes and to support laws for the manipulation of programs.
|