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

Conference paper


Abba, A., Cavalcanti, A. and Jacob, J. 2021. Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata. SBMF 2021: 24th Brazilian Symposium on Formal Methods. Online 06 - 10 Dec 2021 Springer, Cham. https://doi.org/10.1007/978-3-030-92137-8_5
AuthorsAbba, A., Cavalcanti, A. and Jacob, J.
TypeConference paper
Abstract

In this work, we present an approach for automatic translation of tock-CSP into Timed Automata (TA) 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. Automatic verification of TA with a graphical notation is supported by Uppaal. The two approaches provide 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 and a tool based 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 to trace sets. Then, we explore using structural induction to establish the correctness.

Year2021
ConferenceSBMF 2021: 24th Brazilian Symposium on Formal Methods
PublisherSpringer, Cham
Accepted author manuscript
License
File Access Level
Anyone
Publication dates
Online26 Nov 2021
Publication process dates
Deposited01 Dec 2023
Journal citationpp. 70-86
ISSN1611-3349
Book titleFormal Methods: Foundations and Applications: 24th Brazilian Symposium, SBMF 2021, Virtual Event, December 6–10, 2021, Proceedings
Book editorCampos, S.
Minea, M.
ISBN9783030921361
9783030921378
FunderPetroleum Technology Development Fund
Royal Academy of Engineering
Engineering and Physical Sciences Research Council (EPSRC)
Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-030-92137-8_5
Web address (URL) of conference proceedingshttps://link.springer.com/book/10.1007/978-3-030-92137-8
Copyright holder© 2021, The Authors
Copyright informationUse of archived accepted manuscripts (AMs) of non open-access books and chapters are subject to an embargo period and Springer Nature's AM terms of use, which permit users to view, print, copy, download and text and data-mine the content, for the purposes of academic research, subject always to the full conditions of use. Under no circumstances may the AM be shared or distributed under a Creative Commons, or other form of open access license, nor may it be reformatted or enhanced.
Permalink -

https://repository.uel.ac.uk/item/8wz07

Download files


Accepted author manuscript
Paper_SBMF.pdf
License: Springer Nature terms of use for archived author accepted manuscripts (AAMs) of subscription articles, books and chapters
File access level: Anyone

  • 24
    total views
  • 11
    total downloads
  • 3
    views this month
  • 2
    downloads this month

Export as

Related outputs

Fall Detection System with Accelerometer and Threshold-based Algorithm
Tang, D., Usman, A. B. and Abba, A. 2023. Fall Detection System with Accelerometer and Threshold-based Algorithm. YHIoT Research Journal. 1 (1).
Vulnerability prediction for secure healthcare supply chain service delivery
Islam, S., Abba, A., Ismail, U., Mouratidis, H. and Papastergiou, S. 2022. Vulnerability prediction for secure healthcare supply chain service delivery. Integrated Computer-Aided Engineering. 29 (4), pp. 389-409. https://doi.org/10.3233/ICA-220689