Journal
ACTA INFORMATICA
Volume 59, Issue 1, Pages 125-162Publisher
SPRINGER
DOI: 10.1007/s00236-020-00394-3
Keywords
-
Categories
Funding
- EPSRC [EP/M025756/1, EP/R025479/1]
- Royal Academy of Engineering
- EPSRC [EP/R025479/1, EP/M025756/1] Funding Source: UKRI
Ask authors/readers for more resources
The study explores tock-CSP as a dedicated language for modeling budgets, deadlines, and Zeno behavior. It introduces the first tailored semantic model for tock-CSP that captures timewise refinement.
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available