Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata

• Abdulrazaq Abba University of York / University of East London
• Ana Cavalcanti University of York
• Jeremy Jacob University of York

Resumo

We present an approach for automatic translation of tock-CSP into Timed Automata (TA) to facilitate using Uppaal in reasoning about temporal specifications of tock-CSP models. The process algebra tock-CSP provides textual notations for modelling discrete-time behaviours, with the support of tools for automatic verification. Automatic verification of TA with a graphical notation is supported by Uppaal. The two approaches provide diverse facilities for automatic verification. For instance, liveness requirements are difficult to specify with the constructs of tock-CSP, but they are easy to specify and verify in Uppaal. We have developed a translation technique based on rules and a tool for translating tock-CSP into a network of small TAs for capturing the compositional structure of tock-CSP. For validating the rules, we begin with an experimental approach based on finite approximations of trace sets. Then, we consider using structural induction to establish the correctness.

Palavras-chave: Translation, tock-CSP, Timed-Automata