We report the development of a verification tool for Timed CSP processes. The tool has been built on the functional programming language ML. The tool interprets processes described in both timed and untimed CSP, converting them to ML functions, and executing those functions for the verification of refinement in the timed traces and timewise traces models. Using the programmability of higher order functionality, the description of CSP processes with ML has been synthesised naturally. The effectiveness of the tool is demonstrated with an example analysing implementations of Fischer's algorithm for the exclusive control of a shared resource in a multi-processor environment.