Control and synthesis of non-interferent timed systems

DOI10.1080/00207179.2014.944356zbMATH Open1328.93109arXiv1207.4984OpenAlexW2047989760MaRDI QIDQ5265904FDOQ5265904

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)

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

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

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)

Cites Work

• A theory of timed automata
• On observability of discrete-event systems
• Timed control with partial observability.
• 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

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)