Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata - Abba, Abdulrazaq; Cavalcanti, Ana; Jacob, Jeremy (Anais do Simpósio Brasileiro de Métodos Formais (SBMF); 2021: Anais do XXIV Simpósio Brasileiro de Métodos Formais, 2021)
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.