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 non-interference property. 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 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.

In this paper, we focus on distributed systems sub ject to security issues. Such systems are usually composed of two entities: a high level user and a low level user that can both do some actions. The security properties we consider are non-interference properties. A system is non-interferent if the low level user cannot deduce any information by playing its low level actions. Various notions of non-interference have been defined in the literature, and in this paper we focus on two of them: one trace-based property (SNNI) and another bisimulation-based property (BSNNI). For these properties we study the problems of synthesis of a high level user so that the system is non-interferent. We prove that a most permissive high level user can be computed when one exists.

We study some control synthesis problems on an extension of Time Petri Nets that model a plant and its environment. The Time Petri Net control model both represents controllable and uncontrollable events, the problem is then to design a function (controller) such that a given property is fulfilled. We focus our analysis on safety properties expressed on the markings of the net and we propose a symbolic method to decide the existence of a controller that ensures these properties. Unlike existing methods on Time Petri Nets, that assume the net is bounded, the method is applicable for any Time Petri Nets. A consequence is that it is possible to decide the existence of a controller that k-bounds the plant. A method is then proposed to build a state-based controller and problems raised by the implementation (Zenoness, sampling) of the control function on the plant are discussed.

In this paper, we propose a method for building the state class graph of a bounded time Petri net (TPN) as a timed automaton (TA). We consider bounded TPN, whose underlying net is not necessarily bounded. We prove that the obtained TA is timed-bisimilar to the initial TPN. The number of clocks of the automaton is much lower than with other methods available. It allows us to check real-time properties on bounded TPN with efficient TA model-checkers. We have implemented the method, and give some experimental results in this paper, illustrating the efficiency of the algorithm in terms of clock number.

The theory of Petri Nets provides a general framework to specify the behaviour of real-time systems and time extensions have been introduced to take also temporal specifications into account. The main method to compute the state space of a Time Petri Net has been introduced by Berthomieu and Diaz. It is known as the “state class method”. We present in this paper a new efficient method to compute the state space of a bounded Time Petri Net as a marking graph, based on the region graph method used for Timed Automaton. Although some limitations induced by Difference Bounded Matrices (DBM) have been recently discovered by Bouyer in computing the state space of a Timed Automaton (overapproximation), we successfully used DBM in our method. The algorithm is proved to be exact with respect to the reachability of a marking and it computes a graph which nodes are exactly the reachable markings of the Time Petri Net. The tool implemented computes faster than Tina, a tool for computing the state space using classes, and allows to test on-the-fly the reachability of a given marking.

The most widely used approach for verifying the schedulability of a real-time system consists of using analytical methods. However, for complex systems with interdependent tasks and variable execution times, they are not well adapted. For those systems, an alternative approach is the formal modelisation of the system and the use of model-checking, which also allows the verification of more varied scheduling properties. In this paper, we show how an extension of time Petri nets : scheduling extended time Petri nets (SETPN), is especially well adapted for the modelisation of real-time systems and particularly embedded systems and we provide a method for computing the state space of SETPN. We first propose an exact computation using a general polyhedron representation of time constraints, then we propose an overapproximatiion of the polyhedra to allow the use of much more efficient data structures, DBMs. We finally describe a particular type of observers, that gives us a numeric result (instead of boolean) for the computation of tasks response times.