The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach for the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR. We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling.

Hardware Trojan Horses and active fault attacks are a threat to the safety and security of electronic systems. By such manipulations, an attacker can extract sensitive information or disturb the functionality of a device. Therefore, several protections against malicious inclusions have been devised in recent years. A prominent technique to detect abnormal behavior in the field is run-time verification. It relies on dedicated monitoring circuits and on verification rules generated from a set of temporal properties. An important question when dealing with such protections is the effectiveness of the protection against unknown attacks. In this paper, we present a methodology based on automatic generation of monitoring and formal verification techniques that can be used to validate and analyze the quality of a set of temporal properties when used as protection against generic attackers of variable strengths.

In this work, we present an application of symbolic control and contract based design techniques to vehicle platooning. We use a compositional approach based on continuous-time assume-guarantee contracts. Each vehicle in the platoon is assigned an assume-guarantee contract; and a controller is synthesized using symbolic control to enforce the satisfaction of this contract. The assume-guarantee framework makes it possible to deal with different types of vehicles and asynchronous controllers (i.e controllers with different sampling periods). Numerical results illustrate the effectiveness of the approach.

We revisit the problem of finding controlled invariants sets (viability), for a class of differential inclusions, using topological methods based on Wazewski property. In many ways, this generalizes the Viability Theorem approach, which is itself a generalization of the Lyapunov function approach for systems described by ordinary differential equations. We give a computable criterion based on SoS methods for a class of differential inclusions to have a non-empty viability kernel within some given region. We use this method to prove the existence of (controlled) invariant sets of switched systems inside a region described by a polynomial template, both with time-dependent switching and with state-based switching through a finite set of hypersurfaces. A Matlab implementation allows us to demonstrate its use.

Formal methods (e.g. Timed Automata or Linear Hybrid Automata) can be used to analyse a real-time system by performing a reachability analysis on the model. The advantage of using formal methods is that they are more expressive than classical analytic models used in schedulability analysis. For example, it is possible to express state-dependent behaviour, arbitrary activation patterns, etc. In this paper we use the formalism of Linear Hybrid Automata to encode a hierarchical scheduling system. In particular, we model a dynamic server algorithm and the tasks contained within, abstracting away the rest of the system, thus enabling component-based scheduling analysis. We prove the correctness of the model and the decidability of the reachability analysis for the case of periodic tasks. Then, we compare the results of our model against classical schedulability analysis techniques, showing that our analysis performs better than analytic methods in terms of resource utilisation. We further present two case studies: a component with state-dependent tasks, and a simplified model of a real avionics system. Finally, through extensive tests with various configurations, we demonstrate that this approach is usable for medium-size components.

Given a Parametric Timed Automaton (PTA) A and a reference valuation for timings, the Inverse Method (IM) synthesizes a constraint around the reference valuation where A behaves in the same time-abstract manner. This provides us with a quantitative measure of robustness of the behavior of A around the reference valuation. We show in this paper how IM can be applied in a specific way to treat the robustness of scheduling systems. We also explain how to use the method in order to synthesize large zones of the timing parameter space where the system is guaranteed to be schedulable. We illustrate the method on several examples of the literature as well as a case study originating from an industrial design project.

No abstract available.

A procedure that constructs mechanically the appropriate lemmas for proving assertions about programs with arrays is described. A certain subclass of formulas for which the procedure is guaranteed to terminate and thus constitutes a decision procedure is exhibited. This subclass allows for ordering over integers but not for incrementation. A more general subclass that allows for incrementation, but without the termination property, is considered. It is also indicated how to apply the method to a still more general subclass that allows for full arithmetic. These results are extended to the case in which predicates have more than one list argument.>