Control and synthesis of non-interferent timed systems
From MaRDI portal
Publication:5265904
DOI10.1080/00207179.2014.944356zbMATH Open1328.93109arXiv1207.4984OpenAlexW2047989760MaRDI QIDQ5265904FDOQ5265904
Olivier H. Roux, Franck Cassez, Didier Lime, Gilles Benattar
Publication date: 29 July 2015
Published in: International Journal of Control (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1207.4984
Synthesis problems (93B50) Mathematical problems of computer architecture (68M07) Control/observation systems involving computers (process control, etc.) (93C83)
Cites Work
- A theory of timed automata
- On observability of discrete-event systems
- Computer Aided Verification
- Synthesis of opaque systems with static and dynamic masks
- Formalizing non-interference for a simple bytecode language in Coq
- Supervisory control of timed discrete-event systems under partial observation
- Modifying Security Policies for the Satisfaction of Intransitive Non-Interference
Cited In (10)
- Real-Time Control of Dense-Time Systems Using Digital-Clocks
- The complexity of synchronous notions of information flow security
- An optimization-based approach to assess non-interference in labeled and bounded Petri net systems
- Title not available (Why is that?)
- Non-interference assessment in colored net systems via integer linear programming
- Parametric Timed Model Checking for Guaranteeing Timed Opacity
- Optimal controller synthesis for timed systems
- Controller synthesis for dynamic hierarchical real-time plants using timed automata
- Timed non-interference under partial observability and bounded memory
- Synthesis of Non-Interferent Timed Systems
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 👍 👎
- Title not available (Why is that?) 👍 👎
- Template-Based Controller Synthesis for Timed Systems 👍 👎
- Title not available (Why is that?) 👍 👎
- Robust Controller Synthesis in Timed Automata 👍 👎
- A control synthesis approach for time discrete event systems 👍 👎
- Time-Synchronized Control: Analysis and Design 👍 👎
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)
