Formalisation et structuration des architectures opérationnelles pour les systèmes embarqués temps réel

La prise en compte de la complexité croissante des systèmes embarqués temps réel, le besoin de formalisation du processus de développement, les contraintes inhérentes de ces systèmes (ressources limitées et spécifiques, prédictibilité, correction) font qu'il est nécessaire de pouvoir disposer d'un support permettant une maîtrise fine du processus de développement et une gestion sûre des ressources utilisées par le système. L'utilisation des principes de génie logiciel doit permettre de répondre au défi de la maîtrise et de l'amélioration des processus de développement. L'intégration des techniques formelles doit permettre d'assurer la correction des applications produites. Dans les études présentées, nous nous intéressons aux architectures opérationnelles utilisant les services d'un exécutif multitâches. Dans ce cadre, nous avons plus particulièrement exploré deux thèmes. Le premier porte sur l'utilisation des langages SDL et IF et des techniques formelles par modélisation exhaustive pour assurer la correction des systèmes. Le deuxième porte sur l'utilisation du paradigme composant pour la structuration des politiques de gestion de la QdS dans un contexte fortement dynamique. Dans les premiers travaux, un premier niveau, dit de spécification, exprimé en SDL, permet de formaliser les propriétés attendues du système. Ensuite, on décrit, toujours à l'aide de SDL, l'architecture opérationnelle du système par instanciation de boîtes grises, décrivant le comportement des entités du système (tâches, routines). Les modèles IF correspondant fournissent une sémantique d'écoulement du temps. Enfin, les LTS, générés à partir de IF, servent de base à la validation et à la vérification du système. Pour la validation, il faut s'assurer que la mise en place de l'architecture opérationnelle n'aboutit pas à la perte ou à l'activation d'actions non souhaitées. Pour cela nous avons proposé une relation d'équivalence originale qui considère les phénomènes de mémorisation et de décalage temporels inhérent à l'implémentation. Pour la vérification des échéances, l'approche s'appuie sur un modèle réaliste, non abstrait, de l'implémentation (routines d'interruption, sémaphores, boîtes aux lettres, ...) et propose des règles de modélisation et d'abstraction pour contenir le phénomène d'explosion combinatoire (ordre partiel, priorité des tâches, modes de fonctionnement). La vérification, considérant un modèle fin du code, permet par la même occasion de traiter diverses propriétés de sûreté du code (pas de débordement des boîtes aux lettres, ...). Après avoir étudié les langages formels pour décrire et valider des architectures opérationnelles, nous nous intéressons à la structuration à base de composants pour la prise en compte de contraintes de QdS. Dans ce cadre, Fractal et son framework pour l'embarqué Think permettent de construire des systèmes flexibles et adaptables pour les systèmes embarqués. Notre proposition, notée Qinna, permet d'étendre ces modèles pour intégrer des politiques de gestion de la QdS liées à l'utilisation de ressources matérielles. Les expérimentations de Qinna nous ont amené à définir des principes de mise en œuvre, soit des compromis, effectué par le concepteur du système, entre un gaspillage de QdS (discrétisation du niveau de QdS contractualisé) et un nombre important d'opérations d'adaptation à réaliser par l'architecture (suivi de la variabilité des profils de QdS requis et des capacités des ressources matérielles, niveau de QdS contractualisé proche du niveau réel utilisé). Enfin, dans une dernière partie de perspectives, nous donnons des éléments pour étendre les études menées aux architectures applicatives et au plus généralement au problème du déploiement. Dans ce cadre, nous proposons des extensions pour le domaine des systèmes d'acquisition et de communication de données