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
