This Report shows the application of  model checking
techniques over formal specifications expressed in RSL
using the FRD2 refinement checker, for which
we have developed a first version of a translator from
RSL to CSPM.  We give an overview of the semantic 
and syntactic differences between these two languages, 
then we define a translation subset and finally we 
show the strategy used to find the respective equivalences
in order to make the translation possible;
we also briefly describe the development of the translator
and show the use of this translator with some
typical concurrent examples.