Our aim is to exploit the FDR model checker for descriptions of concurrent systems written in the RAISE Specification Language (RSL). To do this we define a translation from RSL to CSPM, show that the translation is a strong bisimulation, and then that various properties are preserved by strong bisimulation. This allows us to infer properties of the RSL description from the results of running FDR.
