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

La prise en compte de la complexite croissante des systemes embarques temps reel, le besoin de formalisation du processus de developpement, les contraintes inherentes de ces systemes (ressources limitees et specifiques, predictibilite, correction) font qu'il est necessaire de pouvoir disposer d'un support permettant une maitrise fine du processus de developpement et une gestion sure des ressources utilisees par le systeme. L'utilisation des principes de genie logiciel doit permettre de repondre au defi de la maitrise et de l'amelioration des processus de developpement. L'integration des techniques formelles doit permettre d'assurer la correction des applications produites. Dans les etudes presentees, nous nous interessons aux architectures operationnelles utilisant les services d'un executif multitâches. Dans ce cadre, nous avons plus particulierement explore deux themes. Le premier porte sur l'utilisation des langages SDL et IF et des techniques formelles par modelisation exhaustive pour assurer la correction des systemes. Le deuxieme 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 specification, exprime en SDL, permet de formaliser les proprietes attendues du systeme. Ensuite, on decrit, toujours a l'aide de SDL, l'architecture operationnelle du systeme par instanciation de boites grises, decrivant le comportement des entites du systeme (tâches, routines). Les modeles IF correspondant fournissent une semantique d'ecoulement du temps. Enfin, les LTS, generes a partir de IF, servent de base a la validation et a la verification du systeme. Pour la validation, il faut s'assurer que la mise en place de l'architecture operationnelle n'aboutit pas a la perte ou a l'activation d'actions non souhaitees. Pour cela nous avons propose une relation d'equivalence originale qui considere les phenomenes de memorisation et de decalage temporels inherent a l'implementation. Pour la verification des echeances, l'approche s'appuie sur un modele realiste, non abstrait, de l'implementation (routines d'interruption, semaphores, boites aux lettres, ...) et propose des regles de modelisation et d'abstraction pour contenir le phenomene d'explosion combinatoire (ordre partiel, priorite des tâches, modes de fonctionnement). La verification, considerant un modele fin du code, permet par la meme occasion de traiter diverses proprietes de surete du code (pas de debordement des boites aux lettres, ...). Apres avoir etudie les langages formels pour decrire et valider des architectures operationnelles, nous nous interessons a la structuration a base de composants pour la prise en compte de contraintes de QdS. Dans ce cadre, Fractal et son framework pour l'embarque Think permettent de construire des systemes flexibles et adaptables pour les systemes embarques. Notre proposition, notee Qinna, permet d'etendre ces modeles pour integrer des politiques de gestion de la QdS liees a l'utilisation de ressources materielles. Les experimentations de Qinna nous ont amene a definir des principes de mise en œuvre, soit des compromis, effectue par le concepteur du systeme, entre un gaspillage de QdS (discretisation du niveau de QdS contractualise) et un nombre important d'operations d'adaptation a realiser par l'architecture (suivi de la variabilite des profils de QdS requis et des capacites des ressources materielles, niveau de QdS contractualise proche du niveau reel utilise). Enfin, dans une derniere partie de perspectives, nous donnons des elements pour etendre les etudes menees aux architectures applicatives et au plus generalement au probleme du deploiement. Dans ce cadre, nous proposons des extensions pour le domaine des systemes d'acquisition et de communication de donnees.