Contexte général
Les systèmes embarqués ont considérablement amélioré la qualité de vie humaine ces trente dernières années et font maintenant partie intégrante de notre quotidien. Leur importance se ressent autant dans la vie active que dans le milieu industriel. Nous les retrouvons dans des petits objets connectés comme les montres intelligentes, les appareils électroménagers jusqu’aux systèmes industriels complexes comme les systèmes aéronautiques, automobiles et de télécommunications. Les systèmes embarqués sont par définition un assemblage de systèmes électroniques et informatiques autonomes destinés à réaliser des tâches précises. Par exemple, dans le domaine automobile, par mesure de sécurité, les véhicules sont équipés de systèmes de freinage automatique ou de détection d’obstacles.
Compte tenu de leur évolution, ces systèmes nécessitent de plus en plus de fonctionnalités tant sur le plan logiciel que matériel en fonction des nouvelles applications mises au point et ceci se traduit par une augmentation de la complexité. Les systèmes embarqués doivent alors implémenter toutes les fonctionnalités souhaitées, être plus performants en ce qui concerne le temps de calcul et exécuter les tâches qui leurs sont attribuées en un temps donné (par ex. systèmes temps réel). Dans le domaine automobile, les nouveaux véhicules intègrent environ 270 fonctions déployées dans 70 unités de commande électronique (ECU) et ce nombre ne cessera de croître dans l’avenir avec les véhicules autonomes. La gestion de toute cette complexité est réalisée par un composant des systèmes embarqués qui sert d’interface entre le matériel et le logiciel, qui implante toutes les fonctionnalités souhaitées et qui est responsable de la gestion des ressources matérielles ainsi que de l’ordonnancement des processus des applications : il s’agit du système d’exploitation. Le système d’exploitation est une solution à la complexité des systèmes embarqués, mais entraîne un coût additionnel de mémoire car, la mémoire représente en effet une forte contrainte pour ces systèmes à cause de leur taille relativement petite. Les systèmes embarqués étant en général de petite taille et présentant des ressources limitées, les systèmes d’exploitation ne peuvent intégrer toutes les fonctionnalités souhaitées pour une large gamme d’application. Par contre, d’une application à une autre, les besoins en terme de fonctionnalités varient. Pour cela, une solution à cette contrainte de taille serait de n’embarquer dans le système d’exploitation que l’ensemble des fonctionnalités réellement nécessaires à une application donnée. Cela aura pour avantage d’optimiser l’espace mémoire occupé par le système d’exploitation, d’améliorer la performance des systèmes embarqués et de réduire la probabilité d’occurrence de comportements fautifs.
Configuration des systèmes d’exploitation
Définitions
La configuration est par définition l’assemblage ou l’organisation d’un ensemble de composants dans le but de former un système complet. Par conséquent, la configuration d’un système d’exploitation permet l’inclusion, l’exclusion ou le remplacement de certaines parties du système d’exploitation. De cette manière, le système d’exploitation peut être « taillé » de façon à répondre aux exigences de l’application, du matériel ou encore de l’utilisateur [Frö01]. Dans un contexte embarqué, plusieurs raisons motivent le choix du développement de systèmes d’exploitation configurables : il s’agit de l’amélioration de la performance des systèmes embarqués, de l’optimisation de l’empreinte mémoire occupée par les systèmes d’exploitation et de l’accroissement de leurs robustesses en ce qui concerne leurs sûretés de fonctionnement etc. D’une part, concernant la charge CPU engendrée par le système d’exploitation, des travaux précédents [BRU+03, HSW+00, KLVA93, KTD+13] ont montré que pour des petits systèmes embarqués jusqu’aux systèmes ayant une puissance de calcul élevée, les systèmes d’exploitation non-configurables ou fixes ont un impact négatif sur la performance des applications. Comme exemple, dans [BRU+03] une comparaison basée sur une étude expérimentale entre le noyau Linux et un système d’exploitation hautement configurable pour des architectures multiprocesseurs a été effectuée et les résultats ont montré que le temps de transfert de message entre deux nœuds de calcul avec le système d’exploitation spécifique est 4 à 10 fois supérieur que celui observé avec le noyau Linux. Toutefois, la configuration de systèmes d’exploitation reste une opération délicate car dans bien des cas, lorsqu’elle est mal réalisée, elle peut causer la dégradation de la performance du système d’exploitation en insérant en son sein des overheads [Frö01].
D’autre part, l’optimisation de la mémoire occupée par les systèmes d’exploitation permet de satisfaire les contraintes de mémoire auxquelles les systèmes embarqués font face car seuls les services indispensables à l’exécution des applications sont pris en compte dans le système d’exploitation. Cela a aussi pour but de réduire la quantité de code inutilisé (source de comportements erronés) au sein des systèmes d’exploitation qui constitue un vecteur privilégié d’attaques. Pour le développement de systèmes d’exploitation configurables, plusieurs critères sont à prendre en compte dont le choix du paradigme de développement, le niveau de granularité souhaité lors de la configuration et l’impact de la configuration sur l’intégrité du système d’exploitation. Dans cette section, nous présenterons en détails ces différents critères.
Paradigme
Le paradigme caractérise non seulement la manière dont est structuré le système d’exploitation mais aussi la manière dont l’application doit être développée. Dans le passé, plusieurs paradigmes ont été utilisés pour le développement de systèmes d’exploitation configurables. Cela va des librairies classiques jusqu’aux objets via les modules et les composants.
Granularité
La granularité définit la finesse de configuration d’un système d’exploitation. Nous pouvons en distinguer deux niveaux à savoir :
— La configuration à gros grain : dans ce type de configuration, on ne peut configurer qu’un sous-système du système d’exploitation. Dans un système d’exploitation ayant une structure basée sur les composants, la configuration à gros grain revient à inclure ou non un composant au sein du système d’exploitation en fonction de son utilité. Par exemple, la configuration du système d’exploitation eCos [Tho00] est basée sur une configuration à gros grain et se fait à l’aide de packages. Le choix de sélection d’un package est fait en fonction des besoins de l’application. D’autres systèmes d’exploitation comme Linux, Scout [Mos97], OSKit [FBB+97] utilisent une configuration à gros grain.
— La configuration à grain fin : ce type de configuration utilise un niveau de configuration plus avancée que la précédente car dans ce cas, il est possible de modifier les fonctions du noyau du système d’exploitation, ses données et même son comportement. Comme exemples de systèmes d’exploitation utilisant une configuration à grain fin, nous pouvons citer MMlite [HF98], Spin [BCE+95] .
Intégrité
L’intégrité est un critère crucial pour les systèmes d’exploitation configurables car elle adresse la question de validité d’une configuration donnée. En effet, pendant l’opération de configuration, des erreurs ou comportements indésirables peuvent être introduits dans le système d’exploitation configuré. Pour assurer l’intégrité d’un système d’exploitation lors de sa configuration, il est nécessaire de mettre en place des mécanismes de vérification (fonctionnelle et temporelle) du système d’exploitation.
Types de configuration
Nous pouvons distinguer deux grandes catégories de configuration, à savoir la configuration statique et la configuration dynamique. Une configuration est définie en fonction de l’étape à laquelle elle intervient dans le cycle de vie d’un système d’exploitation c’est-à-dire à la compilation, à l’édition des liens, à la génération ou à l’exécution du système d’exploitation. La configuration statique est réalisée avant l’exécution du système d’exploitation soit à la compilation, à l’édition de liens ou à la génération du système d’exploitation. En revanche, la configuration dynamique est réalisée pendant l’exécution du système d’exploitation. Chaque type de configuration présente des avantages mais aussi des inconvénients. La configuration statique permet une configuration stable et sûre car généralement réalisée avant l’exécution du système d’exploitation, son intégrité peut être vérifiée avant sa mise en exécution. Ce type de configuration n’engendre pas d’overheads ou encore permet une meilleure utilisation des ressources disponibles puisque tous les besoins en terme de services ou de ressources sont spécifiés avant l’exécution du système d’exploitation. Par contre lorsque le système d’exploitation présente un caractère dynamique c’est-à-dire nécessite de nouvelles fonctionnalités au cours de son exécution, la configuration statique devient inapplicable. C’est pourquoi la configuration dynamique présente un intérêt car elle permet un changement ou une extension des services pendant l’exécution du système d’exploitation en fonction de la demande de l’application.
|
Table des matières
Introduction générale
Chapitre 1 Configuration des systèmes d’exploitation
1.1 Définitions
1.1.1 Paradigme
1.1.2 Granularité
1.1.3 Intégrité
1.2 Types de configuration
1.2.1 Configuration statique
1.2.2 Configuration dynamique
1.3 Paradigme de développement
1.3.1 Programmation orientée objet
1.3.2 Programmation orientée sujet
1.3.3 Programmation orientée aspect
1.3.4 Langages dédiés (DSL)
1.4 Conclusion
Chapitre 2 Trampoline, un système d’exploitation temps réel
2.1 Le standard OSEK/VDX
2.1.1 Architecture du système d’exploitation OSEK
2.1.2 Gestion des tâches
2.1.3 Politique d’ordonnancement
2.1.4 Les modes d’application
2.1.5 Traitement des interruptions
2.1.6 Mécanisme des événements
2.1.7 Gestion des ressources
2.1.8 Alarmes
2.2 AUTOSAR : un standard d’architecture logicielle
2.2.1 Architecture logicielle
2.2.2 Configuration dans AUTOSAR
2.3 Trampoline
2.3.1 Présentation
2.3.2 Architecture de Trampoline monocœur
2.3.3 Architecture de Trampoline multicœur
2.4 Conclusion
Chapitre 3 Modélisation
3.1 Outil de formalisme
3.1.1 Automates finis
3.1.2 Automates finis étendus
3.1.3 Réseau d’automates finis étendus
3.1.4 Utilisation des automates finis étendus pour l’abstraction d’un programme
3.1.5 Accessibilité et bornitude
3.2 Principes de la modélisation
3.2.1 Modélisation des branchements
3.2.2 Modélisation des boucles
3.2.3 Modélisation d’un appel de fonction
3.3 Adaptation à UPPAAL
3.3.1 UPPAAL : outil pour la vérification de systèmes temps réel
3.3.2 Le traitement du temps
3.3.3 Règles de modélisation en utilisant UPPAAL
3.4 Modèle de Trampoline dédié aux architectures monocœur
3.4.1 Modélisation des objets et des variables
3.4.2 Modélisation du noyau
3.4.3 Modélisation des services
3.4.4 Modélisation de l’interruption matérielle liée au timer
3.5 Modèle de Trampoline dédié aux architectures multicœur
3.5.1 Modélisation du noyau
3.5.2 Modélisation des services
3.6 Modèle d’applications
3.7 Propriétés du modèle
3.8 Conclusion
Chapitre 4 Synthèse formelle de systèmes d’exploitation
4.1 Méthodologie
4.1.1 Modélisation
4.1.2 Synthèse formelle
4.1.3 Génération de code
4.2 Outil développé
4.2.1 Synthétiseur de modèle
4.2.2 Générateur de code
4.3 Étude de cas
4.4 Conclusion
Chapitre 5 Vérifications formelles
Conclusion générale