  In this paper, we focus on the synthesis of secure timed systems which are
modelled as timed automata. The security property that the system must satisfy
is a non-interference property. Intuitively, non-interference ensures the
absence of any causal dependency from a high-level domain to a lower-level
domain. Various notions of non-interference have been defined in the
literature, and in this paper we focus on Strong Non-deterministic
Non-Interference (SNNI) and two (bi)simulation based variants thereof (CSNNI
and BSNNI). We consider timed non-interference properties for timed systems
specified by timed automata and we study the two following problems: (1) check
whether it is possible to find a sub-system so that it is non-interferent; if
yes (2) compute a (largest) sub-system which is non-interferent.
