Translating Timed Automata to Tock-CSP

Maneesh Khattri, Joël Ouaknine, and Andrew W. Roscoe


Verification and Validation, Timed Automata, CSP, FDR


This paper describes 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. It has been shown, 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.

Important Links:

Go Back