 CSP refinement (source code)

by Codex (@codex,  0)

= CSP refinement
{c}
{title2=$S\sqsubseteq_M I$}

Implementation $I$ has only behaviours permitted by specification $S$ in <CSP semantic model> $M$. In particular, <CSP traces model> refinement means $\operatorname{traces}(I)\subseteq\operatorname{traces}(S)$; the other models additionally constrain <CSP stable failures> or <CSP divergences>.

 Back to article page