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.

We introduce a simulator (slimsim) for a subset of AADL extended with formalized behavioral semantics for nominal and error models. The simulator allows to perform probabilistic analysis using the Monte Carlo method, on linear-hybrid, stochastic models, which describe a combination of nominal and error behaviors of hard- and software components. The tool supports the use of different strategies, which control the behavior of the simulator when dealing with various forms of non-determinism. The simulator is tested using benchmarks of the COMPASS toolset, as well as a case study by Airbus Defense and Space.

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.

This article studies the scheduling of critical embedded systems, which consist of a set of communicating periodic tasks with constrained deadlines. Currently, tasks are usually sequenced manually, partly because available scheduling policies do not ensure the determinism of task communications. Ensuring this determinism requires scheduling policies supporting task precedence constraints (which we call dependent tasks), which are used to force the order in which communicating tasks execute. We propose fixed priority scheduling policies for different classes of dependent tasks: with simultaneous or arbitrary release times, with simple precedences (between tasks of the same period) or extended precedences (between tasks of different periods). We only consider policies that do not require synchronization mechanisms (like semaphores). This completely prevents deadlocks or scheduling anomalies without requiring further proofs.

Architecture description languages are used to describe both the hardware and software architecture of an application, at system-level. The basic software components are intended to be developed independently, and then deployed on the described architecture. This separate development of the architecture and of the software raises the problem of early validation of the integrated system.

This paper describes a method to verify safety properties of parameterized linear networks of processes. The method is based on the construction of a network invariant, defined as a fixpoint. Such invariants can often be automatically computed using heuristics based on Cousot's widening techniques. These techniques have been implemented and some non-trivial examples are presented.