Up to home page.

The Setting

For the past fifteen years, at Oxford and elsewhere, effort has been spent on the theory and industrial use of formal methods (which have been recognised, for example, by the Queen's awards [QA90] [QA92]). Such methods involve:

Exemplary approaches are those of VDM or Z (see [Mor90, Spi89, Hay87, CBJ88] with the downcoding from Dijkstra's language of guarded commands to Modula 2) and CCS or CSP (see [inm88, Hoa84, Mil89] and the downcoding from CSP to occam and Hardware Description Language, HDL).

The approach of formal methods to the engineering of information systems (software, hardware, or both) has been particularly successful for functional properties --- those that determine the relationship between the system's input, output and state --- and in cases where a hierarchical approach appears natural. A major weakness of the approach is that until recently only functional properties have been thought to be tractable by formal methods, thus leaving informal (or ignoring) attributes like: efficiency (time/space complexity); temporal behaviour; the user interface; inter-user interference; and various forms of failure.

The aim of this project is to incorporate in formal methods one form of failure: deviation from functional behaviour that can be expressed and reasoned about probabilistically.

For example, communications protocols are formalised (indeed standardised) and reasoned about formally (see [VPV92, lot]). One reason for the success of formal methods in this area is that the layers of the ISO standards provide convenient levels of abstraction for describing a design (see [ISO]). Yet the implementations of communications protocols rely ultimately on transmission lines with inherent unreliability (conventionally described statistically). There is thus a gap between the formalisation (which describes only the desired functionality of the protocol) and the implementation (which sometimes violates its specification). This has frequently been interpreted --- not as a successful abstraction of protocol description, but --- as an inherent weakness of formal methods. It is hoped that the present project will encourage a re-evaluation of that interpretation.

The project's more technical components are summarised in the next two sections. It may be viewed as an experiment in the extension of extant formal techniques (of both their supporting theory and realistic application) to incorporate further desirable features: in this case, probability. It will be successful not just when it provides formal description and reasoning about the variety of case studies proposed below, but when the techniques that arise project, when probability is ignored, back to techniques that are already known or make good sense for standard functional methods. For then this specific theory may provide guidelines for how such extensions of present formal methods can be achieved with other system attributes, like those indicated above.

The Approach

In order to be applicable to the specification and development of realistic systems the research of this project must result in a method, or uniform framework enabling it to be applied to a variety of case studies. This section outlines the method and shows how it conforms to (functional) formal methods. Our desire to support it leads to the specific technical goals outlined in the next section.

The method is envisaged as consisting of the following steps, applied incrementally.

  1. Produce a functional specification of the system.

  2. Qualify the functional specification so that all (or part) of it holds to within some reliability tolerance (possible forms for this tolerance are discussed in section 2). Call the resulting specification a probabilistic specification.

  3. Use laws to perform development (also called refinement) of the probabilistic specification. Such laws must support the kinds of steps that software engineers wish to take in order to formalise the design decisions made as a result of their professional experience.

  4. End the development when the specification has been completely expressed in a sublanguage deemed to be implementable (in software, hardware, or some hybrid of the two). Downcode it into executable form. The components of the constructed implementation exhibit probabilistic behaviour, which has been determined during the development and must be met by the implementor.

The Goals

The method described in the previous section is based on the following research, with the first four research goals supporting the method itself.

  1. Probabilistic specification: a notation for specification that incorporates various probabilistic (reliability) tolerances. Here the vague term "probabilistic (reliability) tolerance" has been used to incorporate at least two kinds of phenomena. The first is a predicate that holds with given probability (for example a transmission line described as a 1-place buffer with probability 0.9). The second is a predicate whose distribution is a given distribution function (for example a computer game in which the position of an adversary is described as being normally distributed about a fixed point, with certain mean and variance).

    The probabilistic notation must support incremental, and hence modularised, specification (as in, say, Z). It must describe a wide range of realistic systems. And when the probabilistic term is trivial (for example the probability is 1, or the distribution is a point mass) a probabilistic specification should become the "expected" functional specification.

  2. Probabilistic refinement: a notion of refinement between probabilistic specifications. It should suggest simple, easily-verified sufficient criteria, though there is little hope that these can be as simple as the simulation criteria for functional refinement on which Z and the refinement calculus are based (as in [HHS86]). However when the probabilistic term is trivial the notion should reduce to functional refinement.

    A probabilistic predicate over infinite sequences of actions must be able to be refined by a mechanism that generates just sequences of actions satisfying that predicate; a probabilistic algorithm, for example, would be developed using such an approach. Alternatively, mixing code and specifications, a probabilistic predicate must also be able to be refined by a combination of code and component probabilistically specified which only together meet the specification; communications protocols with inherent errors in the transmission media would be developed using such an approach.

    Support for as many such developments as possible must be provided.

  3. Development rules that ensure probabilistic refinement of one probabilistic specification by another. Soundness must be proved in an appropriate semantic domain (like, for example, those investigated in the DPhil theses [Sei92] and [But92]).

  4. Derived laws: general techniques, found to be useful in the development of probabilistic systems. Though suggested largely by experience with realistic case studies, these must still be proved sound. They may be viewed as cliches of development that occur frequently enough to make worth their recognition, statement and proof.

The next few goals concern the method's application. A variety of examples must be specified, to test the expressive power of the notation for probabilistic specification. For the more difficult task of testing the development method, however, it is proposed to concentrate primarily (though not exclusively) on the development of protocols.

  1. Case studies in specification, demonstrating use of the above specification techniques. These can be expected to range over the wide variety of systems and algorithms that incorporate probability, randomness or uncertainty of outcome, including:
    1. the randomised routing of Valiant [Val82 ]
    2. the probabilistic self-stabilisation of Dijkstra and Hermann [Her90]
    3. the probabilistic algorithms of Rabin et al [Rab91]
    4. the randomised consensus of Herlihy et al [AH90]
    5. probabilistic algorithms expressed in UNITY [Rao94].

  2. Case studies in development. For the more difficult task of development some specialisation of subject area will, to be realistic, be required. Though development of the specifications above will be considered, special attention will be paid to the development of communications protocols. That decision has been motivated by our concern to convince practicioners of the use of our method. As discussed above, formal methods have already proved useful in standardising communications protocols and there are indications that protocol designers will be receptive to extensions of their techniques that incorporate probability. Case studies in development will thus include any of the examples from (a) above, but may be expected to concentrate on:
    1. describing network behaviour at a level of abstraction much greater than that at which a particular protocol operates [Kin90]
    2. existing communications protocols
    3. existing communications protocols to derive new probabilistic tolerances
    4. the design of new protocols that are either easier to develop in the probabilistic formalism, or can be proved optimal in a sense that the formalism enables to be made explicit.

  3. Modules. It is to be expected that several modules, or abstract data types, may be conveniently explained and developed using probabilistic formalism. At present they are specified and developed using the pre/post notation, and their probabilistic behaviour is treated informally. It would be far more satisfying to teach both aspects within the same formalism; it would also provide a test of the formalism. For example, exercise the probabilistic formalism on the specification and development of the module: hash table implementation of a set module, whose probabilistic behaviour is well known-see [Knu73])-but can now be incorporated in the development formalism.

The remaining goals relate to the nature of the probabilistic predicate. Investigate the shape of probabilistic tolerances: (a) acceptable in an implementation; and (b) desirable in a specification.

  1. For example in transmission media, errors are quantified using standard distributions, so it is expected that those distributions will find a place in the implementation of communications protocols. However elsewhere in information engineering less standard distributions arise (in summary, they tend to be skewed when uniformity might have been expected); see [PS83, AB57, Knu73]. It would be interesting to study the range of distributions that occur in protocols and various other systems.

  2. Having identified the "target" distributions for a development it would be interesting to see what developments give rise to it. This approach is analogous to one that has been successful in other disciplines, where modelling assumptions are made that give rise to observed distributions (for example, [Kol41, BS81, AB57]); our "modelling assumptions" appear in the specification and are discharged in the development.

  3. The previous point can be summarised as the bottom-up study of distributions: what assumptions give rise to previously-identified distributions in the implementation? A top-down study would also be of interest: making natural assumptions in the specification, development gives rise to what type of tolerance in the lower-level designs (and implementation)? Then the formalism may suggest new tolerances where before only electrical-engineering convenience or tradition prevailed.

  4. Subsume, in probabilistic tolerance, the various notions of fairness (see [Fra86]), and refine the reasoning done about systems using those less expressive notions.

Conclusion

The conventional route to the design of programs and even programming languages has been from the bottom up: given hardware, a programming language is designed whose features are inherited from the hardware (for example, FORTRAN). Then programs are written-even applications identified as programmable-based on the characteristics of that programming language. In some cases, at the last stage, a semantics is proposed for the language concerned (for example, ADA). The defects of that approach are well known.

Successful reversal of the above is indicated, for example, by the increased interest in the design of special-purpose hardware for the execution of functional or logic languages, or for graphical applications. A more startling example is provided by the sequence: CSP (semantics first), occam (the programming language), transputer (and finally hardware on which to execute programs).

The situation regarding probability is analogous: at present we are limited to accepting systems whose probabilistic behaviour is determined by the engineers who design it, expressed in forms most suitable to them. Repetition of the strategy above may permit redesign of the low-level "toolkit", and may reap analogous benefits. It may cost little to express the probabilistic component of a system design in a different way (different-though still well known-distributions); or different aspects of the behaviour of probabilistic constraints. It would save much if that new way facilitates rigorous reasoning and development targeted towards it.