Dans les domaines critiques d'application de l'informatique, il peut être vital de disposer d'un génie logiciel qui soit capable de garantir le bon fonctionnement des systèmes produits. Dans ce contexte, la méthode B évènementielle promeut le développement de modèles abstraits du système à concevoir et l'utilisation de démonstrations formelles ainsi que de la relation de raffinement entre les modèles. Notre but est de pouvoir travailler sur des systèmes ayant des aspects temporels quantitatifs (propriétés et contraintes de temps) en restant au sein du cadre défini par la méthode B qui a déjà montré son efficacité par ailleurs, mais qui ne dispose pas de concepts spécifiques pour le temps. C'est ainsi que nous proposons l'introduction des contraintes de temps par le raffinement, ceci permet de respecter la philosophie de la méthode B et de systématiser cette approche par la formalisation de patrons de raffinement. Nos différentes modélisations du temps sont proposées sous la forme de patron à réappliquer sur le système à étudier. Nous pouvons donc étudier progressivement le système à partir d'une abstraction non-temporelle afin de le valider progressivement et de distribuer la difficulté de la preuve en plusieurs étapes. L'introduction des aspects temporels ne se fait que lorsque cela est nécessaire lors du processus de développement prouvé. Nous avons validé cette approche sur des études de cas réalistes en utilisant les outils logiciels de démonstration formelle de la méthode B.

Au cours de ces dernières décennies, les systèmes technologiques ont beaucoup évolué. Dans le même temps, leurs installations sont de plus en plus distribuées sur plusieurs sites. Ceci conduit à la résolution de problèmes logistiques lors des prises de décision en vue d'actions de maintenance qui exigent par ailleurs des approches coopératives dans un contexte de gestion à distance. Dans ce travail, nous étudions des méthodes d'aides à la décision temps-réel pour la maintenance des systèmes multi-sites distribués dans un environnement à ressources partagées, avec des contraintes logistiques non négligeables entre les différents sites. Les exigences sont de planifier et d'ordonnancer les tâches de maintenance, de les affecter en temps-réel aux ressources de maintenance disponibles, tout en minimisant les coûts inhérents au fonctionnement et en maîtrisant les délais d'intervention des ressources. Les coûts sont relatifs notamment au fonctionnement en état dégradé (état critique), aux fréquences trop élevées ou au déficit de maintenance. Ils dépendent aussi de combinaisons linéaires ou convexes d'ensemble de paramètres tels que les temps de réponse (temps de séjour), les retards et avances ainsi que des facteurs de pondération des tâches de maintenance. Les coûts sont également fonction de la disponibilité, cette dernière étant révélatrice des dégradations des entités constituant le système. Pour satisfaire ces exigences, différents problèmes doivent être résolus dans le but de maintenir la disponibilité du système au dessus d'une limite minimale, de minimiser le coût des opérations de maintenance et d'affecter en temps-réel les tâches aux ressources de maintenance, le tout dans un processus optimal de décision. Ce processus doit tenir compte de différentes contraintes : dates d'arrivée inégales des tâches, temps logistiques non négligeables entre les sites, séquences optimales des tâches d'une intervention, précédences entre les tâches d'une même entité et critères de priorité et d'urgence de chaque tâche. Dans cette démarche, les caractéristiques et lois de comportement en fiabilité et en maintenabilité, et les sollicitations d'intervention sur les entités sont connues. Pour résoudre ces problèmes, nous proposons une approche mettant en oeuvre des méthodes d'ordonnancement d'activités (tâches ou actions) de maintenance basées sur des règles de priorité dont nous montrons l'optimalité locale (par rapport au temps) dans ce document. Partant d'une ressource de maintenance, ces règles de décision s'inspirent des principes d'ordonnancement sur une seule machine. Elles sont utilisées dans des algorithmes d'aide à la décision en temps-réel pour la planification dynamique des tâches de maintenance des systèmes distribués. Aux solutions fournies par la plupart de ces règles nous avons déterminé des bornes inférieures. Nous avons structuré ce document en six chapitres dont le premier introduit de façon générale la maintenance et ses différentes pratiques dans les entreprises. Le chapitre 2 propose une analyse de l'état de l'art des travaux de recherche scientifique dans le domaine de la gestion des activités de maintenance. Ensuite, dans le chapitre 3, des approches de résolution des problèmes relatifs aux coûts des états critiques du système sont proposées. Le chapitre 4 traite alors les différents problèmes relatifs aux contraintes de délais sur les opérations de maintenance induisant notamment des coûts combinés liés aux états critiques et aux retards d'intervention d'une part, et des coûts dus aux avances ou retards des tâches d'autre part. Il apparut alors nécessaire d'étudier la robustesse des performances des approches proposées dans les chapitres 3 et 4 en environnements incertains. Cette étude fût donc réalisée dans le chapitre 5 par des simulations Monte Carlo de la maintenance à partir des données d'un système réel soumis à des aléas de défaillance appelant des actions correctives. Enfin, de l'ensemble des investigations menées dans ce travail furent tirées les principales conclusions et les perspectives proposées dans le chapitre 6.

Le cadre de ce travail est l'étude coordonnée de lois de contrôle et d'ordonnancement. Le premier objectif est de proposer et évaluer une approche de contrôle de la dégradation de la Qualité de Contrôle (QdC) par rejet sélectif d'instances de tâches ou de messages selon le<br />modèle (m,k)-firm. Plus particulièrement, nous avons étudié l'impact de distribution de rejets sur la QdC d'une boucle de contrôle et, sur la base des résultats obtenus, nous avons spécifié une méthode de co-conception permettant de déterminer les paramètres (gain) optimaux de la loi de contrôle et les paramètres de la contrainte (m,k)-firm spécifiant le rejet sélectif d'instances. Cette proposition a été validée sur modèles à l'aide de techniques analytiques, par simulation ainsi que grâce à des expérimentations. Notre deuxième objectif est d'étudier le problème de l'ordonnancement d'un ensemble de tâches temps réel réalisant chacune les algorithmes de contrôle dans une application centralisée évolutive. Nous proposons un mécanisme d'ordonnancement qui ajuste en ligne les contraintes<br />(m,k)-firm des tâches suivant la configuration courante de l'application de manière à ce qu'un critère reflétant la performance globale de l'application soit optimal à tout instant.

Dans le cadre de cette thèse, nous nous proposons d'étudier le développement et la validation de systèmes dans un contexte temps réel asynchrone. On a choisi d'utiliser le langage AADL pour ses spécificités issues de l'avionique, domaine proche du spatial, et pour la précision de la description de son modèle d'exécution. Le travail de cette thèse se divise en deux axes principaux : d'une part, on étudie l'utilisation du langage AADL dans le cadre du développement d'un logiciel de vol ; et d'autre part, on présente une version réduite du langage AADL, et la définition formelle de son modèle d'exécution à l'aide du langage TLA+. L'objectif de la première partie est d'envisager l'utilisation d'AADL dans le cadre d'un processus de développement existant dans le domaine du spatial. Dans cette partie, on a cherché à identifier des motifs de conceptions récurrents dans les logiciels de vol. Enfin, on étudie l'expression en AADL des différents éléments de ce processus de développement. La seconde partie comporte la définition d'un mini AADL suffisant pour exprimer la plupart des concepts de parallélisme, de communication et de synchronisation qui caractérisent AADL. La partie formalisation est nécessaire afin de pouvoir vérifier des propriétés dynamiques. En effet, la définition formelle du modèle d'exécution permet de décrire le comportement attendu des modèles AADL. Une fois ce modèle défini, on peut à l'aide d'un vérificateur de modèles (model-checker) animer une modélisation AADL ou aborder la vérification de propriétés dynamiques. Cette étude a par ailleurs été menée dans le cadre de la standardisation du langage AADL.

A rapidly growing computer graphics community has contributed to dramatic increase in complexity with respect to geometry as well as physical phenomena. Simulating, approximating and visualizing geometry consisting of tens of millions of polygons simultaneously tested for collision or visibility is becoming increasingly common. Further, recent technological innovations from graphics card vendors have given impetus to achieving these results at very high frame rates. Despite tremendous developments in graphics hardware, capturing the complete surrounding environment poses a significant challenge. Given the added time constraint for real-time or interactive rates, simplified representations and suitable approximations of physical effects are of key importance.<br /><br />This dissertation focuses on simplified representations and computations to achieve real-time performance for complex tasks and concentrates on a variety of topics including simplification, visibility, soft shadows and voxelization.

Lustre est un langage de programmation spécialement conçu pour la réalisation des systèmes réactifs. Le besoin de garantir que ces systèmes ont un comportement conforme a celui attendu nécessite de définir et de mettre en œuvre des méthodes de vérification formelle des programmes lustre, qui sont relatées dans cette thèse. La vérification d'un système consiste a contrôler que tous ses comportements sont corrects vis-a-vis de ses spécifications. Les comportements d'un programme lustre peuvent classiquement être représentés par une machine d'états finis, dont la génération permet de vérifier ses spécifications. La methode standard mettant en œuvre ce principe est limitée par le probleme d'explosion de la machine générée, qui n'est pas minimale. Un nouvel algorithme évitant ce probleme est présenté. Son implémentation nécessite l'emploi d'une technique de représentation et de manipulation symbolique de la machine (bdds), dont le cout d'utilisation est largement abaisse grâce a de nombreuses optimisations. Basées sur cette technique, deux autres implémentations originales de la methode standard et de la nouvelle methode proposée ci-dessus sont décrites. Les aspects de diagnostic correspondant au cas ou les programmes sont incorrects vis-a-vis de leurs spécifications sont aussi abordes

Dans le cadre de cette thèse, nous nous intéressons à la vérification de systèmes réactifs critiques et temps réel développés a l'aide de langages flots de données synchrones. Plus particulièrement nous avons considéré les propriétés de sureté pour les applications réalisées dans un des deux langages, saga produit de Merlin Gerin/ses, ou lustre crée au LGI. La méthode de vérification, pour laquelle un prototype a été réalise, est l'évaluation de propriétés sur un modèle des programmes. Un langage de spécification adapte au contexte des systèmes réactifs temps réel, avec sa sémantique formelle, est défini; ce langage comprend plusieurs opérateurs temporels. Le désir d'automatiser la vérification a nécessité la définition de la sémantique formelle de saga. Plusieurs modèles pour les programmes ont alors été étudiés: les arbres des exécutions comme base d'expression commune des sémantiques, les graphes d'états et automates de contrôle pour la mise en œuvre de la vérification. L'utilisation de moyens existants de vérification, fondée sur l'évaluation de propriétés sur un modèle des programmes, a été étudiée et évaluée. Ces moyens sont relatifs a des logiques temporelles arborescentes et des mu-calculs propositionnels. Une nouvelle approche pour la spécification et la vérification de propriétés de sureté, mettant en œuvre les caractéristiques du langage lustre, est développée. Elle s'appuie sur l'utilisation de lustre lui-même comme langage de spécification et présente les avantages suivants: formalisme commun pour la programmation et la spécification, utilisation du compilateur pour la vérification, possibilité de preuves modulaires

Ce manuscrit présente une méthode de contrôle de qualité de service à grain fin d'applications multimédia. Celle-ci permet le contrôle d'applications dont les actions sont paramétrées par des niveaux de qualité et dont les durées d'exécution ne sont pas connues. Le contrôle consiste en la construction d'un ordonnancement et le choix des niveaux de qualité respectant des propriétés de sûreté et d'optimalité. C'est-à-dire que l'on cherche à maximiser l'utilisation du budget de temps sans pour autant le dépasser tout en ayant un choix de qualité régulier. Le contrôleur utilise une politique de gestion de qualité permettant de choisir pour chaque action l'ordonnancement et le niveau de qualité respectant les contraintes de qualité de service. Nous étendons et améliorons les résultats précédents dans deux directions. La première propose une approche symbolique de la politique de gestion de qualité. Celle-ci utilise un diagramme de vitesses qui est une représentation graphique du comportement de l'application contrôlée. À partir de cette représentation, nous avons proposé une technique de contrôle permettant de relâcher le nombre d'appels au contrôleur tout en respectant les propriétés de sûreté et d'optimalité. Nous avons ensuite proposé une approche stochastique du problème basée sur des fonctions de distribution de probabilités pour les durées d'exécution des actions. Notre méthode donne la possibilité à l'utilisateur de fixer la criticité des contraintes temps-réel. Elle permet aussi de calculer à priori le taux attendu de dépassement des échéances. Ces résultats théoriques ont été appuyés par des expériences réalisées sur un encodeur vidéo s'exécutant sur machine nue.

Notre proposition consiste à présenter un modèle et une infrastructure d'exécution orienté composant pour le domaine des applications multi-tâches à contraintes temps réel souples et embarquées (nommé Tinap).<br /><br />Nous définissons un modèle de composant reposant sur plusieurs vues : une vue structurelle, placée au centre du cycle de conception, reposant initialement sur le modèle Fractal, une vue dynamique permettant au concepteur, dans une démarche descriptive, de personnaliser l'architecture métier pour définir les aspects de son applicatif liés à la concurrence, et enfin une vue implantation et une vue comportement fournissant respectivement une abstraction de l'implantation interne des composants et de leur comportement à l'égard de leur environnement. De plus, notre proposition est intégrée à un cadre méthodologique dirigé par les modèles.<br /><br />Nous avons également expérimenté le paradigme composant à différents niveaux d'abstraction : pour l'applicatif et pour celui de l'infrastructure d'exécution qui les implante. Enfin, au niveau du système d'exploitation fournissant les services élémentaires nécessaires. Cette démarche est motivée par la volonté d'exploiter notre modèle multi-vues canonique et de l'adapter en fonction des besoins de chaque niveau d'abstraction. Cette expérimentation est menée avec Think, une implantation en C des spécifications Fractal.<br /><br />Nous expérimentons Tinap par deux cas d'étude que nous avons prototypés. En premier lieu, pour concevoir une application d'analyse et de contrôle de flux multimédias par l'intermédiaire de disques vinyles. En second lieu pour expérimenter la mise en oeuvre du modèle d'exécution Accord (une méthodologie de conception pour applications temps-réel).

Une methode de conception descendante par affinements successifs de spécifications est présentée. Le point de départ de la conception est la spécification initiale du système sous forme comportementale. L'étape suivante est la specification algorithmique du systeme qui consiste à définir une machine abstraite réalisant le systeme ainsi que la dérivé temporelle admissible sur les entrées et les sorties du système. Ensuite, deux types d'implantation sont proposes: l'implantation fidèle qui est la réalisation d'une machine concrète ayant un comportement semblable à la machine abstraite (à la dérivé temporelle près). Dans le cas contraire, une alarme est envoyée à l'environnement. Cette implantation peut être faite automatiquement grâce à l'interpréteur GRAFCET fidèle. Le deuxième type d'implantation est l'implantation sur ou par construction les contraintes de fonctionnement sont respectées