In the field of computer security, a problem that received little attention so far is enforcement confidentiality properties by supervisory control. Given critical system <i xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">G</i> may leak confidential information, consists in designing controller xmlns:xlink="http://www.w3.org/1999/xlink">C</i> , possibly disabling occurrences fixed subset events closed-loop / does not information. We consider this...

In this paper, we are interested in the diagnosis of discrete event systems modeled by finite transition systems. We propose a model supervision patterns general enough to capture past occurrences particular trajectories system. Modeling objective pattern allows us generalize properties be diagnosed and render them independent description first formally define problem context. then derive techniques for construction diagnoser verification diagnosability based on standard operations show that...

We consider feedback control systems where sensor readings may be compromised by a malicious attacker intending on causing damage to the system. study this problem at supervisory layer of system, using discrete event techniques. assume that can edit outputs from sensors system before they reach controller. In context, we formulate synthesizing supervisor is robust against class attacks and present solution methodology for problem. This blends techniques games automata with imperfect...

We describe the extension of a reactive programming language with behavioral contract construct. It is dedicated to control applications in embedded systems, and involves principles supervisory discrete event systems. Our contribution approach where modular controller synthesis (DCS) integrated, it concretized encapsulation DCS into compilation process. From transition system specifications possible behaviors, automatically produces controllers that make controlled satisfy property given as...

Given a finite transition system and regular predicate, we address the problem of computing controller enforcing opacity predicate against an attacker (that partially observes system), supposedly trying to push reveal predicate. Assuming that can only control subset events it (possibly different from ones attacker), show optimal always exists provide sufficient conditions under which is effectively computable. These rely on inclusion relationships between observable alphabets controllable alphabet.

In this paper, we describe a methodology integrating verification and conformance testing. A specification of system - an extended input-output automaton, which may be infinite-state set safety properties ("nothing bad ever happens") possibility ("something good happen") are assumed. The first tentatively verified on the using automatic techniques based approximated state-space exploration, sound, but, as price to pay for automation, not complete given class properties. Because...

We consider feedback control systems where sensor readings may be compromised by a malicious attacker intent on causing damage to the system. study this problem at supervisory layer of system, using discrete event techniques. assume that can edit outputs from sensors system before they reach controller. In context, we formulate synthesizing supervisor is robust against large class attacks readings. solve new methodology improves upon prior work topic. The solution based partially observed...

The UML Profile for Modeling and Analysis of Real-Time Embedded systems (MARTE) defines a mathematically expressive model time, the Clock Constraint Specification Language (CCSL), to specify timed annotations on diagrams thus provides them with formally defined interpretations. Thanks its capability, CCSL allows specification static dynamic properties, deterministic non-deterministic behaviors, or multiple clock domains. Code generation from such multi-clocked specifications (for purpose...

This paper investigates the supervisor synthesis for concurrent systems based on reduced system models with intention of complexity reduction. It is assumed that expected behavior (specification) given a subset alphabet, and to this alphabet. Supervisors are computed each subsystem employing modular approach in Komenda et al. (2005) decentralized Lee Wong (2002). Depending chosen architecture, we provide sufficient conditions consistent implementation supervisors original

In this paper, we investigate the control of infinite systems, modeled by symbolic transition system for safety properties. We first redefine concept controllability applying it to guards transitions, instead events. then define synthesis algorithms based on transformations and abstract interpretation techniques so that can ensure finiteness computations.