Automated Translation of Timed Automata to Tock CSP

I will describe the automated translation of timed automata to tock-CSP. This translation has been implemented in a translator. The tock-CSP output of the translator can be input into FDR for the automated verification of properties of the input timed automata. I will show, by the use of the digitisation technique, that there are relationships between Timed Automata and tock-CSP. Preliminary experiments indicate that this technique is promising for the automated verification of real-time systems and should be further developed.