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

TL;DR

This paper presents a translation method and tool for converting tock-CSP models into Timed Automata to leverage UPPAAL's verification capabilities for temporal specifications, addressing differences in modeling and verification approaches.

Contribution

It introduces a novel translation technique and supporting tool for converting tock-CSP into Timed Automata, enabling the use of UPPAAL for temporal reasoning.

Findings

Developed translation rules for tock-CSP to Timed Automata

Validated the translation through experimental finite approximations

Proved the correctness of translation rules for infinite traces

Abstract

In this work, we consider translating tock-CSP into Timed Automata for UPPAAL 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. Similarly, automatic verification of Timed Automata (TA) with a graphical notation is supported by the UPPAAL real-time verification toolbox \uppaal. The two modelling approaches, TA and tock-CSP, differ in both modelling and verification approaches, temporal logic and refinement, respectively, as well as their provided 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. To take advantage of temporal logic, we translate tock-CSP into TA for \uppaal; we have developed a translation technique and its supporting tool. We provide rules for translating tock-CSP into a network of small TAs for capturing the compositional structure of tock-CSP that is not available in TA. For validation, we start with an experimental approach based on finite approximations to trace sets. Then, we explore mathematical proof to establish the correctness of the rules for covering infinite traces.