Skip to main content


Synthesis of non-interferent timed systems


Gilles Benattar, Franck Cassez, Didier Lime and Olivir Henri Roux





In this paper, we focus on the synthesis of secure timed systems which are given by timed automata. The security property that the system must satisfy is a \emph{non-interference} property. Various notions of non-interference have been defined in the literature, and in this paper we focus on \emph{Strong Non-deterministic Non-Interference} (SNNI) and we study the two following problems: ($1$) check whether it is possible to enforce a system to be SNNI; if yes ($2$) compute a sub-system which is SNNI.

BibTeX Entry

    publisher        = {Lecture Notes in Computer Science},
    author           = {Benattar, Gilles and Cassez, Franck and Lime, Didier and Roux, Olivir Henri},
    month            = oct,
    editor           = {{J. Ouaknine and F. Vandraager}},
    year             = {2009},
    keywords         = {security, timed automata, synthesis},
    title            = {Synthesis of Non-Interferent Timed Systems},
    booktitle        = {Proc. of the 7th Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS'09)},
    pages            = {28--42},
    address          = {Budapest, Hungary}