Gavin Lowe
1992, 39pp.
In a previous paper [TR-24-91] we presented two new models of timed CSP. The first model included biased operators in the syntax, which could be used to model different priorities on actions. The second model extended this by adding a probabilistic choice operator to the syntax; this allowed us to give a semantics which modelled the probabilities of different behaviours occurring. In TR-17-92, we presented another new model, which used biased operators but did not include probabilistic choice. We presented an abstraction mapping from the probabilistic, prioritized model to the unprobabilistic, prioritized model.
In this paper we want to relate the prioritized model to the timed failures model. We will investigate which failures could have resulted from a particular prioritized behaviour, and thus produce an abstraction mapping from the prioritized model to the failures model.
We will study how this result can be used to prove that a process satisfies its specification. We will show that if a process in the failures model satisfies a particular specification, then all its prioritized refinements satisfy a related specification. This will simplify many of our proofs by allowing them to be carried out in the (simpler) failures model.