Paper Details

Communicating Process Architectures (CPA)
 Title: The Meaning and Implementation of SKIP in CSP
 Conference: Communicating Process Architectures 2013
 Authors: Thomas Gibson-Robinson, Michael Goldsmith
Department of Computer Science, University of Oxford
 Abstract: The CSP model checker FDR has long supported Hoare’s termination semantics for CSP, but has not supported the more theoretically complete construction of Roscoe's, largely due to the complexity of adding a second termination semantics. In this paper we provide a method of simulating Roscoe's termination semantics using the Hoare termination semantics and then prove the equivalence of the two different approaches. We also ensure that FDR can support the simulation reasonably efficiently. 

BibTeX Entry

Full paper