In "On the Expressiveness of CSP", Roscoe provides a construction that, given the operational semantics rules of a CSP-like language and a process in that language, constructs a strongly bisimilar CSP process. Unfortunately, the construction provided is difficult to use and the scripts produced cannot be compiled by the CSP model-checker, FDR. In this paper, we adapt Roscoe's simulation to make it produce a process that can be checked relatively efficiently by FDR. Further, we extend Roscoe's simulation in order to allow recursively defined processes to be simulated in FDR, which was not supported by the original simulation. We also describe the construction of a tool that can automatically construct the simulation, given the operational semantics of the language and a script to simulate, both in an easy-to-use format.
展开▼
