  The process algebra tock-CSP provides textual notations for modelling
discrete-time behaviours, with the support of various tools for verification.
Similarly, automatic verification of Timed Automata (TA) is supported by the
real-time verification toolbox UPPAAL. TA and tock-CSP differ in both modelling
and verification approaches. For instance, liveness requirements are difficult
to specify with the constructs of tock-CSP, but they are easy to verify in
UPPAAL. In this work, we translate tock-CSP into TA to take advantage of
UPPAAL. We have developed a translation technique and tool; our work uses rules
for translating tock-CSP into a network of small TA, which address the
complexity of capturing the compositionality of tock-CSP . For validation, we
use an experimental approach based on finite approximations to trace sets. We
plan to use mathematical proof to establish the correctness of the rules that
will cover an infinite set of traces.
