| Summary: | Les logiciels embarqués critiques de contrôle-commande sont soumis à des contraintes fortes englobant le déterminisme, la correction logique et la correction temporelle. Nous supposons que les spécifications sont exprimées à l'aide du langage formel de description d'architectures logicielles temps réel multipériodiques Prelude. L'objectif de cette thèse est, à partir d'un programme Prelude ou d'un ensemble de tâches temps réel dépendantes, de générer un code multithreadé exécutable sur une architecture multicœur tout en respectant la sémantique initiale. Pour cela, nous avons développé une boîte à outil, SchedMCore,permettant : - d'une part, la vérification formelle de l'ordonnançabilité. La vérification proposée est basée sur le parcours exhaustif du comportement avec pas de temps discret. Il est alors possible d'analyser des politiques en-ligne (FP, gEDF, gLLF et LLREF) mais également de calculer une affectation de priorité fixe valide et une séquence valide hors-ligne.- d'autre part, l'exécution multithreadée sur une cible multicœur. L'exécutif encode les politiques proposées étudiées dans la partie d'analyse d'ordonnançabilité, à savoir les quatre politiques en-ligne ainsi que les séquences valides générées. L'exécutif permet 3 modes d'utilisation, allant de la simulation temporelle à l'exécution temps précis des comportements des tâches. Il est compatible Posix et facilement portable sur divers OS. === A real-time control-command embedded system is subject to strong constraints such as determinism, logical and temporal correctness. We assume that the specifications are expressed using the formal software architecture description language Prelude, dedicated to real-time multiperiodic applications. The goal of this thesis is, given a Prelude program or dependent real-time taskset, to generate amultithreaded executable code over a multicore architecture while respecting the original semantic. To do so we have developed a toolbox, SchedMcore, that allows: - the formal verification of schedulability. The verification is based on the exhaustive exploration of the behaviour with a discret time frame. It is possible to analyse on-line policies (FP, gEDF, gLLF et LLREF), as well as to compute a fixed valid priority assignment and a valid off-line sequence.- the multithreaded execution over a multicore target. The framework encodes the same policies as those studied in the first part (the four on-line policies and the generated sequences). The framework provides three usage modes, from temporal simulation to time accurate execution. The executive is compatible with Posix and easily portable on several OS.
|
|---|
