We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Automatic Translation of tock-CSP into Timed Automata

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.
Comments: An updated version of this paper is available in this link arXiv:2104.13434
Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)
Cite as: arXiv:2008.06935 [cs.LO]
  (or arXiv:2008.06935v2 [cs.LO] for this version)

Submission history

From: Abdulrazaq Abba [view email]
[v1] Sun, 16 Aug 2020 15:23:43 GMT (1273kb,D)
[v2] Thu, 29 Apr 2021 09:33:52 GMT (0kb,I)

Link back to: arXiv, form interface, contact.