Priorities in tock-CSP
share
The tock-CSP encoding embeds a rich and flexible approach to modelling discrete timed behaviours in CSP where the event tock is interpreted to mark the passage of time. The model checker FDR provides tailored support for tock-CSP, including a prioritisation operator that has typically been used to ensure maximal progress, where time only advances after internal activity has stabilised. Prioritisation may also be used on its own right as a modelling construct. Its operational semantics, however, is only congruent over the most discriminating semantic model of CSP: the finite-linear model. To enable sound and compositional reasoning in a tock-CSP setting, we calculate a denotational definition for prioritisation. For that we establish a Galois connection between a specialisation of the finite-linear model, with tock and , that signals termination, as special events, and -tock-CSP, a model for tock-CSP that captures termination, deadlines, and is adequate for reasoning about timed refinement. Our results are mechanised using Isabelle/HOL.
READ FULL TEXT