Gavin Lowe
1992, 49pp.
In a previous paper [TR-24-91] we presented two new languages based upon timed CSP, with associated semantic models. The first language was a completely deterministic language, which included biased operators that can be used to model different priorities on actions. The second language extended this by adding a probabilistic choice operator to the syntax; this allowed us to give a semantics that modelled the probabilities of different behaviours occurring.
In this paper we study methods of specifying and proving correct such processes. We shall restrict our attention to hard specifications, i.e. specifications that hold of all behaviours of a process. This means that we will not actually consider probabilities -- this will be the subject of a future paper. We concentrate on specifying and proving correct processes that make use of prioritized actions.
We present a new language which includes biased operators but not probabilities, and give the language a semantic model. We give abstraction mappings from the probabilistic and deterministic models to the unprobabilistic, biased model. This allows us to show that one can prove that a probabilistic or deterministic process meets a hard specification by proving that the corresponding unprobabilistic process meets the same specification.
We then examine ways of proving that specifications are met in the (unprobabilistic) prioritized model. We present a specification language that allows one to specify, for example, that events are performed at certain times, or that particular priorities are given to actions. We then present a number of proof rules that can be used for proving that a process meets a specification; for compound processes, the proof obligation is reduced to proof obligations upon the subcomponents. The proof system is illustrated with a couple of examples.