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

TY - GEN

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

AU - Abba, Abdulrazaq

AU - Cavalcanti, Ana

AU - Jacob, Jeremy

N1 - Funding Information: Abba gratefully acknowledges the financial support of Petroleum Technology Development Fund (PTDF). Cavalcanti is funded by the Royal Academy of Engineering grant CiET1718/45 and the UK EPSRC grants EP/M025756/1 and EP/R025479/1. Funding Information: Acknowledgements. Abba gratefully acknowledges the financial support of Publisher Copyright: © 2021, Springer Nature Switzerland AG.

PY - 2021/11/26

Y1 - 2021/11/26

N2 - 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.

AB - 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.

KW - Timed-Automata

KW - tock-CSP

KW - Translation

UR - http://www.scopus.com/inward/record.url?scp=85121912105&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-92137-8_5

DO - 10.1007/978-3-030-92137-8_5

M3 - Conference contribution

AN - SCOPUS:85121912105

SN - 9783030921361

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 70

EP - 86

BT - Formal Methods

A2 - Campos, Sérgio

A2 - Minea, Marius

PB - Springer Science and Business Media Deutschland GmbH

T2 - 24th Brazilian Symposium on Formal Methods, SBMF 2021

Y2 - 6 December 2021 through 10 December 2021

ER -