Skip to main content

Completing CSP

Bill Roscoe ( OUCL )

After adding a natural new operator to CSP that is related to interrupt, we are able to show that no further operator can be required. Specifically, we define what it means for an operator to have a CSP-like operational semantics, and show that every such operator is expressible using the extended language.

A side benefit of this is that it becomes possible to define new operators operationally, confident that they have congruent definitions over the semantic models and fit naturally into CSP's refinement framework.

Share this: