By the same authors

From the same journal

Sound reasoning in tock-CSP

Research output: Contribution to journalArticlepeer-review

Full text download(s)

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

JournalActa Informatica
DateAccepted/In press - 5 Dec 2020
DateE-pub ahead of print (current) - 17 Apr 2021
Early online date17/04/21
Original languageEnglish

Abstract

Specifying budgets and deadlines using a process algebra like CSP requires an explicit notion of time. The tock-CSP encoding embeds a rich and flexible approach for modelling discrete-time behaviours with powerful tool support. It uses an event tock, interpreted to mark passage of time. Analysis, however, has traditionally used the standard semantics of CSP, which is inadequate for reasoning about timed refinement. The most recent version of the model checker FDR provides tailored support for tock-CSP, including specific operators, but the standard semantics remains inadequate. In this paper, we characterise tock-CSP as a language in its own right, rich enough to model budgets and deadlines, and reason about Zeno behaviour. We present the first sound tailored semantic model for tock-CSP that captures timewise refinement. It is fully mechanised in Isabelle/HOL and, to enable use of FDR4 to check refinement in this novel model, we use model shifting, which is a technique that explicitly encodes refusals in traces.

Bibliographical note

Funding Information:
This work is funded by EPSRC Grants EP/M025756/1 and EP/R025479/1, and by the Royal Academy of Engineering. No new primary data was created as part of the study reported here.

© 2021, The Author(s).

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations