Translating timed automata to tock-CSP

Journal article

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.

Authors: Khattri, M; Ouaknine, J; Roscoe, A

• Journal: Proceedings of the 10th IASTED International Conference on Software Engineering, SE 2011
• Pages: 9-17
• Publication date: 2011-01-01
• DOI: 10.2316/P.2011.720-047
• Language: English
• Keywords: Verification and validation; CSP; Timed automata; FDR