Automatic Translation of tock-CSP into Timed Automata

TL;DR

This paper presents a translation method and tool to convert tock-CSP models into Timed Automata, enabling the use of UPPAAL for verification of discrete-time behaviors and liveness properties.

Contribution

It introduces a novel translation technique from tock-CSP to Timed Automata, facilitating verification with UPPAAL and addressing compositionality challenges.

Findings

Developed a translation tool and rules for tock-CSP to TA conversion

Validated the approach using finite trace set approximations

Plans for mathematical proof of correctness for infinite traces

Abstract

The process algebra tock-CSP provides textual notations for modelling discrete-time behaviours, with the support of various tools for verification. Similarly, automatic verification of Timed Automata (TA) is supported by the real-time verification toolbox UPPAAL. TA and tock-CSP differ in both modelling and verification approaches. For instance, liveness requirements are difficult to specify with the constructs of tock-CSP, but they are easy to verify in UPPAAL. In this work, we translate tock-CSP into TA to take advantage of UPPAAL. We have developed a translation technique and tool; our work uses rules for translating tock-CSP into a network of small TA, which address the complexity of capturing the compositionality of tock-CSP . For validation, we use an experimental approach based on finite approximations to trace sets. We plan to use mathematical proof to establish the correctness of the rules that will cover an infinite set of traces.