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
Publicado
07/12/2021
ABBA, Abdulrazaq; CAVALCANTI, Ana; JACOB, Jeremy. Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata. In: SIMPÓSIO BRASILEIRO DE MÉTODOS FORMAIS (SBMF), 24. , 2021, Campina Grande. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2021 . p. 70-86.