Checking Noninterference in Timed CSP

A well established noninterference property in untimed CSP is that lazily abstracting high-level actions leaves a deterministic process. This is problematic in Timed CSP (both continuous and discrete) because there are then many refinement maximal properties that are not deterministic. This phenomenon is a result of No Instantaneous Withdrawal (NIW): if a process offers an event b up to time t, then b is still possible AT time t. We give exact characterisations of maximality in continuous and discrete Timed CSP in terms of the extended idea of Quasi-Determinism, and justify an alternative definition of noninterference in terms of these.

By generalising Ouaknine's theory of digitisation for Timed CSP we are able to establish the following curious result: an integer Timed CSP process P is noninterfering as judged over the continuous model of Timed CSP if and only if the process 2P (which runs exactly half as fast) is quasi-deterministic over the discrete model.

We show how to check this property in the Timed CSP model of FDR 2.94 and give an example.

[A draft of this paper can be found on my website. This work builds on the doctoral work of Huang Jian.]