= Concurrency
{scope}
{title2=A10405W1}
Solutions to all three questions of the examination dated 1 June 2015. The cover permits answers to two questions.<Concurrency examination paper by the University of Oxford (2015)>[Cover; questions on printed pp. 2–5]{ref}
Throughout, $\Sigma$ is the visible <CSP event> alphabet, $\tau$ is a <CSP internal action>, and $\mathrm{STOP}$ has no transitions. There is no successful termination event. Write $S\sqsubseteq_M I$ when implementation $I$ refines specification $S$ in model $M$: the implementation's recorded behaviours are contained in the specification's. We use $T$, $F$ and $FD$ for the <CSP traces model>, <CSP stable-failures model> and <CSP failures-divergences model>.
Back to article page
