Méthode de génération d’exécutif temps-réel

In embedded systems, specialization or configuration of real-time operating systems according to the application requirements consists to remove the operating system services that are not needed by the application. This operation allows both to optimize the memory footprint occupied by the real-time operating system in order to meet the memory constraints in embedded systems and to reduce the amount of dead code inside the real-time operating system in order to improve its reliability. In this thesis, we focus on the use of formal methods to specialize real-time operating systems according applications. One major difficulty using formal models is the gap between the system model and its implementation. Thus, we propose to model the operating system so that the model embeds its source code and manipulated data structures. For this purpose, we use finite state model (possibly timed model) with discrete variables and sequences of instructions which are considered as atomic manipulating these variables. From the operating system model and an application model, the set of reachable states of the operating system model describing the code needed during application execution is computed. Thus, the source code of the specialized operating system is extracted from the pruned model. The overall approach is implemented with Trampoline, a real-time operating system based on OSEK/VDX and AUTOSAR standards. This specialization technique ensures the absence of dead code, minimizes the memory footprint and provides a formal model of the operating system used in a last step to check its behavior by using model checking. In this context, we propose an automatic formal verification technique that allows to check the operating systems according OSEK/VDX and AUTOSAR standards using generic observers.Dans les systèmes embarqués, la spécialisation ou la configuration des systèmes d’exploitation temps réel en fonction des besoins de l’application consiste en la suppression des services inutiles du système d’exploitation. Cela a non seulement pour but d’optimiser l’empreinte mémoire occupée par le système d’exploitation temps réel, afin de satisfaire les contraintes de mémoire auxquelles les systèmes embarqués font face, mais aussi de réduire la quantité de code mort au sein du système d’exploitation temps réel afin d’améliorer la sureté de fonctionnement. Dans nos travaux de thèse, nous nous intéressons à l’utilisation des méthodes formelles dans le processus de spécialisation des systèmes d’exploitation temps réel. Une difficulté majeure dans l’utilisation de modèles formels est la distance entre le modèle et le système modélisé. Nous proposons donc de modéliser le système d’exploitation de telle sorte que le modèle embarque son code source et les structures de données manipulées. Nous utilisons à cet effet un modèle à états finis (éventuellement temporisé) augmenté par des variables discrètes et des séquences d’instructions, considérées comme atomiques, manipulant ces variables. À partir du modèle du système d’exploitation et d’un modèle de l’application visée, l’ensemble des états accessibles du modèle du système d’exploitation traduisant le code effectivement utilisé lors de l’exécution de l’application est calculé. Le code source du système d’exploitation spécialisé est extrait de ce modèle élagué. L’ensemble de la démarche exposée est mise en oeuvre avec Trampoline, un système d’exploitation temps réel basée sur les standards OSEK/VDX et AUTOSAR. Cette technique de spécialisation garantit l’absence de code mort, minimise l’empreinte mémoire et fournit un modèle formel du système d’exploitation utilisable dans une étape ultérieure de modelchecking. Dans ce cadre, nous proposons une technique automatique de vérification formelle de la conformité aux standards OSEK/VDX et AUTOSAR à l’aide d’observateurs génériques