Control and synthesis of non-interferent timed systems

DOI10.1080/00207179.2014.944356MaRDI QIDQ5265904zbMATH OpenOpenAlexFDO

Authors Gilles Benattar, Franck Cassez, Didier Lime, Olivier H. Roux

Publication date 29 July 2015

Published in International Journal of Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1207.4984

zbMATH Keywords

synthesiscontrolnon-interferencetimed automatonsafety timed games

Mathematics Subject Classification ID

Synthesis problems (93B50) Mathematical problems of computer architecture (68M07) Control/observation systems involving computers (process control, etc.) (93C83)

Abstract: 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.

Recommendations

• Synthesis of Non-Interferent Timed Systems
• Optimal controller synthesis for timed systems
• On the synthesis of discrete controllers for timed systems
• Non-interference control synthesis for security timed automata
• scientific article; zbMATH DE number 1301632
• Template-based controller synthesis for timed systems
• scientific article; zbMATH DE number 2086417
• Robust Controller Synthesis in Timed Automata
• A control synthesis approach for time discrete event systems
• Time-synchronized control: analysis and design

Cites work

• A theory of timed automata
• Formalizing non-interference for a simple bytecode language in Coq
• Modifying Security Policies for the Satisfaction of Intransitive Non-Interference
• On observability of discrete-event systems
• Supervisory control of timed discrete-event systems under partial observation
• Synthesis of opaque systems with static and dynamic masks
• Timed control with partial observability.

Cited in

(13)

• An optimization-based approach to assess non-interference in labeled and bounded Petri net systems
• Information flow for timed automata
• Real-Time Control of Dense-Time Systems Using Digital-Clocks
• Controller synthesis for dynamic hierarchical real-time plants using timed automata
• The complexity of synchronous notions of information flow security
• Timed non-interference under partial observability and bounded memory
• Synthesis of Non-Interferent Timed Systems
• Non-interference assessment in colored net systems via integer linear programming
• Optimal controller synthesis for timed systems
• Non-interference control synthesis for security timed automata
• Parametric Timed Model Checking for Guaranteeing Timed Opacity
• Secure information release in timed automata
• scientific article; zbMATH DE number 1799514 (Why is no real title available?)

This page was built for publication: Control and synthesis of non-interferent timed systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5265904)