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.
| Original language | English |
|---|---|
| Pages (from-to) | 126-162 |
| Journal | Acta Informatica |
| Volume | 59 |
| DOIs | |
| Publication status | Published - 17 Apr 2021 |
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).