Paper Details

Efficient Simulation of CSP-Like Languages

Authors: Gibson-Robinson, Thomas

Abstract:

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.

Proceedings:

Communicating Process Architectures 2013, Peter H. Welch, Frederick R. M. Barnes, Jan F. Broenink, Kevin Chalmers, Jan Bækgaard Pedersen, Adam T. Sampson, 2013, pp 185 - 204 published by Open Channel Publishing Ltd., Bicester

Files: Paper (PDF), Slides (PDF)

This record in other formats:

Web page: BibTEX, Refer
Plain text: BibTEX, Refer

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.