La synthèse logique joue un rôle fondamental dans les compilateurs de silicium. Alors que l'état de l'art de la synthèse deux couches est très avance, celui de la synthèse multi-couches reste encore un sujet très ouvert. L'objet de cette thèse est de présenter des méthodes originales de synthèse de contrôleurs et de systèmes combinatoires pour une implémentation multi-couches a base de cellules de bibliothèque. Le premier chapitre définit le concept de compilation de silicium et introduit l'une de ses composantes, la synthèse logique. L'importance du marche de la synthèse logique y est clairement définie ainsi que ses implications dans la conception actuelle de circuits intégrés. Le deuxième chapitre concerne la synthèse de contrôleurs. Le probleme du codage des machines d'états fini est traite en détail et une methode basée sur la théorie d'immersion de cubes intersectant dans un hypercube booléen est proposée. Le troisième chapitre est consacre a la synthèse de circuits combinatoires et une methode d'optimisation temporelle de tels dispositifs est développée. Ces travaux ont été implémentés dans un environnement industriel

L'Internet des Objets (IdO) et les Environnements Intelligents (EI) ont attiré beaucoup d'activités de recherche et développement au cours de la dernière décennie. Pourtant, de nombreuses applications IdO/EI d'aujourd'hui sont encore limitées à l'acquisition et au traitement des données de capteurs et de leur contexte, avec un contrôle, le cas échéant, utilisant soit des solutions de base ou demandant l'intervention humaine, loin du contrôle automatique qui est un facteur essentiel de promouvoir ces technologies. Cette thèse vise à apporter le savoir-faire de la théorie du contrôle et des systèmes réactifs dans le domaine IdO/EI pour arriver à une solution avec une méthode formelle pour l'aspect de contrôle qui fait défaut. Nous proposons l'extension d'un canevas logiciel pour une infrastructure générique et partagée IdO/EI qui offre des interfaces de haut niveau pour réduire l'effort de conception, et qui permet l'auto-configuration et l'adaptation des applications de contrôle sur des propriétés génériques de l'environnement sans intervention humaine en utilisant les connaissances générales sur le domaine qui s'appliquent à chaque instance cible de système IdO/EI. Dans cette infrastructure étendue, les entités physiques individuelles (y compris toutes les "choses", appareils électriques et sous-ensembles de l'espace) peuvent être regroupées comme des entités virtuelles par des propriétés communes afin de fournir un niveau d'abstraction plus élevé pour le contrôle et d'autres applications, ainsi qu'une meilleure adaptation aux changements des configurations au niveau inférieur. Sur le requis d'une solution générique et commun dénominateur partagée par toutes les applications de l'IdO/EI dans un environnement donné, nous proposons pour cette infrastructure, de modéliser les entités cibles supervisées et contrôlées, y compris les entités individuelles et de leurs regroupements, ainsi que les choses et les entités spatiales, par des automates à états finis, pour être en mesure d'appliquer la technique de la synthèse des contrôleur discrets (SCD) aux différents niveaux d'abstraction et de granularité. SCD est une méthode formelle qui construit automatiquement un contrôleur, s'il existe, en assurant les objectifs de contrôle exigés concernant le modèle de comportement du système donné en termes d'automates parallèles synchrones. Les langages de programmation BZR et les outils Sigali existants sont utilisés pour effectuer la SCD et de générer un contrôleur de manière automatique. Les modules logiciels nécessaires sont proposés dans l'implémentation tels que le module de maintenance de relation qui garde une association correcte entre les instances d'entités individuelles et les groupes, et répercute des commandes d'action du contrôle de haut niveau aux actionneurs correspondants. Ce module est destiné à évoluer plus tard vers une solution plus générique comme une base de données graphes comprenant à la fois la base de connaissances générales et relations spécifiques d'instance environnement. La résolution des conflits entre les objectifs de contrôle venant de contrôleurs concurrent est également indispensable en raison des objectifs de l'ouverture de la plateforme. Un simulateur de contexte basé sur Java a été développé pour simuler l'environnement de la maison au sein de plusieurs scénarios proposés pour la validation, tels que le contrôle de la charge électrique et l'adaptation au contexte de l'activité. / The Internet of Things (IoT) and Smart Environments (SE) have attracted a lot of research and development activities during the last decade. Yet many present-day IoT/SE applications are still limited to the acquisition and processing of sensor data and its context, with control, if any, using either basic solutions or requiring human intervention, far away from the automatic control which is an essential factor to promote the technologies. This thesis targets to bring knowhow from control theory and reactive systems to the IoT/SE domain to achieve a solution with a formal method for the missing control aspect. We propose the extension of a framework in order to build a shared generic IoT/SE infrastructure offering high-level interfaces to reduce design effort, and enabling the self-configuration and adaptation of control applications over generic properties of the environment without human interaction by using general knowledge over the domain that applies to each target instance of IoT/SE system. In this extended framework, individual physical entities (including all relevant "things", appliances and subsets of space) may be grouped as virtual entities by shared properties to provide a higher level abstraction for control and other applications and better adaptation to lower level configuration changes. Requiring a generic common denominator solution shared by all IoT/SE applications in a given environment, we propose for this infrastructure, to model by finite state automata the target entities to be monitored and controlled, including both individual entities and their groupings, as well as things and space entities, to be able to apply discrete controller synthesis (DCS) technique over any of these at different levels of abstraction and granularity. DCS is a formal method which constructs automatically a controller, if it exists, guaranteeing the required control objectives regarding to the given system behavior model in terms of synchronous parallel automata. The existing BZR programming language and Sigali tools are employed to perform DCS and generate a controller in an automatic way. Necessary supporting software modules are proposed in the implementation such as the relation maintenance module keeping the correct association between individual entity instances and groups, and dispatching the action orders from the high level control to corresponding actuators. This module would evolve later to a more generic solution such as a graph data base including both the general knowledge base and specific environment instance relations. Conflict resolution between objectives of control coming from concurrent controllers is also indispensable due to the intended openness of the platform. A java based context simulator has been developed to simulate the home environment within several scenarios proposed for the validation, such as electrical load control and activity context adaptation.

L'Internet des Objets (IdO) et les Environnements Intelligents (EI) ont attiré beaucoup d'activités de recherche et développement au cours de la dernière décennie. Pourtant, de nombreuses applications IdO/EI d'aujourd'hui sont encore limitées à l'acquisition et au traitement des données de capteurs et de leur contexte, avec un contrôle, le cas échéant, utilisant soit des solutions de base ou demandant l'intervention humaine, loin du contrôle automatique qui est un facteur essentiel de promouvoir ces technologies. Cette thèse vise à apporter le savoir-faire de la théorie du contrôle et des systèmes réactifs dans le domaine IdO/EI pour arriver à une solution avec une méthode formelle pour l'aspect de contrôle qui fait défaut. Nous proposons l'extension d'un canevas logiciel pour une infrastructure générique et partagée IdO/EI qui offre des interfaces de haut niveau pour réduire l'effort de conception, et qui permet l'auto-configuration et l'adaptation des applications de contrôle sur des propriétés génériques de l'environnement sans intervention humaine en utilisant les connaissances générales sur le domaine qui s'appliquent à chaque instance cible de système IdO/EI. Dans cette infrastructure étendue, les entités physiques individuelles (y compris toutes les "choses", appareils électriques et sous-ensembles de l'espace) peuvent être regroupées comme des entités virtuelles par des propriétés communes afin de fournir un niveau d'abstraction plus élevé pour le contrôle et d'autres applications, ainsi qu'une meilleure adaptation aux changements des configurations au niveau inférieur. Sur le requis d'une solution générique et commun dénominateur partagée par toutes les applications de l'IdO/EI dans un environnement donné, nous proposons pour cette infrastructure, de modéliser les entités cibles supervisées et contrôlées, y compris les entités individuelles et de leurs regroupements, ainsi que les choses et les entités spatiales, par des automates à états finis, pour être en mesure d'appliquer la technique de la synthèse des contrôleur discrets (SCD) aux différents niveaux d'abstraction et de granularité. SCD est une méthode formelle qui construit automatiquement un contrôleur, s'il existe, en assurant les objectifs de contrôle exigés concernant le modèle de comportement du système donné en termes d'automates parallèles synchrones. Les langages de programmation BZR et les outils Sigali existants sont utilisés pour effectuer la SCD et de générer un contrôleur de manière automatique. Les modules logiciels nécessaires sont proposés dans l'implémentation tels que le module de maintenance de relation qui garde une association correcte entre les instances d'entités individuelles et les groupes, et répercute des commandes d'action du contrôle de haut niveau aux actionneurs correspondants. Ce module est destiné à évoluer plus tard vers une solution plus générique comme une base de données graphes comprenant à la fois la base de connaissances générales et relations spécifiques d'instance environnement. La résolution des conflits entre les objectifs de contrôle venant de contrôleurs concurrent est également indispensable en raison des objectifs de l'ouverture de la plateforme. Un simulateur de contexte basé sur Java a été développé pour simuler l'environnement de la maison au sein de plusieurs scénarios proposés pour la validation, tels que le contrôle de la charge électrique et l'adaptation au contexte de l'activité. / The Internet of Things (IoT) and Smart Environments (SE) have attracted a lot of research and development activities during the last decade. Yet many present-day IoT/SE applications are still limited to the acquisition and processing of sensor data and its context, with control, if any, using either basic solutions or requiring human intervention, far away from the automatic control which is an essential factor to promote the technologies. This thesis targets to bring knowhow from control theory and reactive systems to the IoT/SE domain to achieve a solution with a formal method for the missing control aspect. We propose the extension of a framework in order to build a shared generic IoT/SE infrastructure offering high-level interfaces to reduce design effort, and enabling the self-configuration and adaptation of control applications over generic properties of the environment without human interaction by using general knowledge over the domain that applies to each target instance of IoT/SE system. In this extended framework, individual physical entities (including all relevant "things", appliances and subsets of space) may be grouped as virtual entities by shared properties to provide a higher level abstraction for control and other applications and better adaptation to lower level configuration changes. Requiring a generic common denominator solution shared by all IoT/SE applications in a given environment, we propose for this infrastructure, to model by finite state automata the target entities to be monitored and controlled, including both individual entities and their groupings, as well as things and space entities, to be able to apply discrete controller synthesis (DCS) technique over any of these at different levels of abstraction and granularity. DCS is a formal method which constructs automatically a controller, if it exists, guaranteeing the required control objectives regarding to the given system behavior model in terms of synchronous parallel automata. The existing BZR programming language and Sigali tools are employed to perform DCS and generate a controller in an automatic way. Necessary supporting software modules are proposed in the implementation such as the relation maintenance module keeping the correct association between individual entity instances and groups, and dispatching the action orders from the high level control to corresponding actuators. This module would evolve later to a more generic solution such as a graph data base including both the general knowledge base and specific environment instance relations. Conflict resolution between objectives of control coming from concurrent controllers is also indispensable due to the intended openness of the platform. A java based context simulator has been developed to simulate the home environment within several scenarios proposed for the validation, such as electrical load control and activity context adaptation.

La méthode des invariants est une des plus utilisées méthodes de synthèse pour les SED modélisés par des réseaux de Petri (RdP). Cependant, elle ne garantit pas en général une solution optimale dans la présence de l'incontrôlabilité. Dans ce travail nous proposons une solution à ce problème pour les RdP généralisés. Premièrement, nous proposons une solution d'identification des contraintes admissibles pour les RdP saufs non-conservatifs. La méthode repose sur une définition des contraintes contenant des marquages complémentés. Ceux-ci sont après éliminés en exploitant les composants conservatifs des RdP. Deuxièmement, nous avançons une technique de détermination des contraintes admissibles pour les RdP généralisés. La méthode est basée sur une vision spatiale de l'espace d'états du modèle. Les contraintes sont dérivées de l'équation d'hyperplan affin qui sépare les régions interdite- et autorisée- de cet espace. Nous proposons un algorithme pour le calcul du contrôleur optimal minimal. / The place-invariants method is one of the most popular controller synthesis approaches for Petri net (PN) modeled DES. Unfortunately, the observance of the constraints is not certain in the presence of uncontrollable transitions. This thesis offers a solution to this problem for ordinary and generalized PNs. We begin by studying safe non-conservative PNs, and devising a constraint-determination technique that will always provide a set of admissible constraints for this type of model. The approach stems from the general definition of forbidden states --- that of marking vectors. In the second part of our work, we present an admissible constraint-determination technique for generalized PNs. The method is based on a special view of the system's state space. The constraints are derived from the equation of the affine hyper-plane separating the authorized- and forbidden- regions of this space. We propose an algorithm that allows the identification of the minimal maximally permissive controller.

Dans cette thèse nous proposons un cadre formel complet pour l'analyse des systèmes temporisés, avec l'accent mis sur la valeur pratique de l'approche. Nous décrivons des systèmes comme des automates temporisés et nous exprimons les propriétés en logiques temps-réel. Nous considérons deux types d'analyse. Vérification : étant donnés un système et une propriété, vérifier que le système satisfait la propriété. Synthèse de contrôleurs : étant donnés un système et une propriété, restreindre le système pour qu'il satisfasse la propriété. Pour rendre l'approche possible malgré la difficulté théorique des problèmes, nous proposons : Des abstractions pour réduire l'espace d'états concret en un espace abstrait beaucoup plus petit qui, pourtant, préserve toutes les propriétés qui nous intéressent. Des techniques efficaces pour calculer et explorer l'espace d'états abstrait. Nous définissons des bisimulations et simulations faisant abstraction du temps et nous étudions les propriétés qu'elles préservent. Pour les bisimulations, l'analyse consiste à générer d'abord l'espace abstrait, et ensuite l'utiliser pour vérifier des propriétés sur l'espace concret. Pour les simulations, la génération et la vérification se font en même temps (à-la-volée). Un algorithme à-la-volée est aussi développé pour la synthèse de contrôleurs. Pour aider l'utilisateur à sa compréhension du système, nous produisons des séquences diagnostiques concrètes. Nous avons implanté nos méthodes dans Kronos, l'outil d'analyse temps-réel de Verimag, et nous avons traité un nombre d'études de cas réalistes parmi lesquelles le protocole FRP-DT de réservation rapide de débit pour les réseaux ATM (dans le cadre d'une coopération scientifique avec le CNET), le protocole de détection de collisions dans un réseaux à accès multiple de Band&Olufsen, l'ordonnancement de tâches temps-réel périodiques, la cohérence et l'ordonnancement des documents multimédia, ainsi qu'un nombre d'études de cas benchmarks, telles que le protocole d'exclusion mutuelle de Fischer, les protocoles de communication CSMA/CD et FDDI.

Dans cette thèse, nous nous intéressons à la spécification et à la synthèse de contrôleurs des systèmes temps-réels. Les modèles pour ces systèmes sont des Event-recording Automata. Nous supposons que les contrôleurs observent tous les évènements se produisant dans le système et qu'ils peuvent interdirent uniquement des évènements contrôlables. Tous les évènements ne sont pas nécessairement contrôlables. Une première étude est faite sur la logique Event-recording Logic (ERL). Nous proposons des nouveaux algorithmes pour les problèmes de vérification et de satisfaisabilité. Ces algorithmes présentent les similitudes entre les problèmes de décision cité ci-dessus et les problèmes de décision similaires étudiés dans le cadre du $\mu$-calcul. Nos algorithmes corrigent aussi des algorithmes présents dans la littérature. Les similitudes relevées nous permettent de prouver l'équivalence entre les formules de ERL et les formules de ERL en forme normale disjonctive. La logique ERL n'étant pas suffisamment expressive pour décrire certaines propriétés des systèmes, en particulier des propriétés des contrôleurs, nous introduisons une nouvelle logique WT$_\mu$. La logique WT$_\mu$ est une extension temps-réel faible du $\mu$-calcul. Nous proposons des algorithmes pour la vérification des systèmes lorsque les propriétés sont écrites en WT$_\mu$. Nous identifions deux fragments de WT$_\mu$ appelés WT$_\mu$ bien guardé ($WG$-WT$_\mu$) et WT$_\mu$ pour le contrôle ($C$-WT$_\mu$). La logique $WG$-WT$_\mu$ est plus expressif que $C$-WT$_\mu$. Nous proposons un algorithme qui permet de vérifier si une formule de $WG$-WT$_\mu$ possède un modèle (éventuellement déterministe). Cet algorithme nécessite de connaître les ressources (horloges et constante maximale comparée avec les horloges) des modèles. Dans le cadre de $C$-WT$_\mu$ l'algorithme que nous proposons et qui permet de décider si une formule possède un modèle n'a pas besoin de connaître les ressources des modèles. En utilisant $C$-WT$_\mu$ comme langage de spécification des systèmes, nous proposons des algorithmes de décision pour le contrôle centralisé et le $\Delta$-contrôle centralisé. Ces algorithmes permettent aussi de construire des modèles de contr\^oleurs. Lorsque les objectifs de contrôle sont décrits à l'aide des formules de $WG$-WT$_\mu$, nous montrons également comment synthétiser des contrôleurs décentralisés avec des ressources fixées à l'avance et ceci, lorsqu'au plus un contrôleur est non déterministe. / In this dissertation, we consider the specification and the controller synthesis problem for real-time systems. Our models for systems are kinds of Event-recording automata. We assume that controllers observe all the events occurring in the system and can prevent occurrences of controllable events. We study Event-recording Logic (ERL). We propose new algorithms for the model-checking and the satisfiability problems of that logic. Our algorithms are similar to some algorithms proposed for the same problems in the setting of the standard $\mu$-calculus. They also correct earlier proposed algorithms. We define disjunctive normal form formulas and we show that every formula is equivalent to a formula in disjunctive normal form. Unfortunately, ERL is rather weak and can not describe some interesting real-time properties, in particular some important properties for controllers. We define a new logic that we call WT$_\mu$. The logic WT$_\mu$ is a weak real-time extension of the standard $\mu$-calculus. We present an algorithm for the model-checking problem of WT$_\mu$. We consider two fragments of WT$_\mu$ called well guarded WT$_\mu$ ($WG$-WT$_\mu$) and WT$_\mu$ for control ($C$-WT$_\mu$). We show that the satisfiability of $WG$-WT$_\mu$ is decidable if the maximal constants appearing in models are known a priori. Our algorithm allows to check whether a formula of $WG$-WT$_\mu$ has a deterministic model. The algorithm we propose to decide whether a formula of $C$-WT$_\mu$ has a model does not need to know the maximal constant used in models. All the algorithms for the satisfiability checking construct witness models. Using $C$-WT$_\mu$, we present algorithms for a centralised controller synthesis problem and a centralised $\Delta$-controller synthesis problems. The construction of witness controllers is effective. We also consider the decentralised controller synthesis problem with limited resources (the maximal constants used in controllers is known a priory) when the properties are described with $WG$-WT$_\mu$. We show that this problem is decidable and the computation of witness controllers is effective.

La synthèse de contrôleurs discrets (SCD) est appliquée pour générer automatiquement des contrôleurs matériels corrects par construction. Pour un système donné (un modèle à états), et une spécification de contrôle associée (une exigence comportementale), cette technique génère un contrôleur qui, composé avec le système initial, garantit la satisfaction de la spécification. La technique de SCD utilisée dans ce travail s’appuie sur les diagrammes de décision binaire (BDDs). Les contrôleurs générés doivent être compatibles avec les outils standards de synthèse matérielle de niveau RTL. Deux problèmes principaux ont été examinés: l’explosion combinatoire et la génération effective du contrôleur matériel. La maîtrise de l’explosion combinatoire s’appuie sur des approches de type «diviser pour régner », exploitant la modularité du système ou du contrôleur. La plupart des approches existantes ne traitent pas la communication explicite entre différents composants du système. Le mécanisme de synchronisation le plus couramment envisagé est le partage des événements d’entrée, faisant abstractiondes sorties. Nous proposons une technique de SCD incrémentale qui permet de traiter également les systèmes communicants. Une étape initiale d’abstraction modulaire est suivie par une séquence progressive de raffinements et de calculs de solutions approximatives de contrôle. La dernière étape de cette séquence engendre un contrôleur exact. Nous montrons que cette technique offre une efficacité améliorée en temps/mémoire par rapport à l’approche traditionnelle globale de la SCD. La génération du contrôleur matériel s’appuie sur un traitement spécifique du non-déterminisme de contrôle. Une architecture de contrôle à boucle partiellement fermée est proposée, afin de permettre une conception hiérarchique. Une technique automatique transformant une équation de contrôle en vecteur de fonctions de contrôle est proposée et illustrée. La SCD est ensuite appliquée et illustrée sur la correction de certaines erreurs de conception. L’efficacité des techniques proposées est illustrée sur un ensemble d’exemples de conception matérielle. / The Discrete Controller Synthesis (DCS) technique is used for automatic generation of correct-by-construction hardware controllers. For a given plant (a state-based model), and an associated control specification (a behavioral requirement), DCS generates a controller which, composed with the plant, guarantees the satisfaction of the specification. The DCS technique used relies on binary decision diagrams (BDDs). The controllers generated must be compliant with standard RTL hardware synthesis tools. Two main issues have been investigated: the combinational explosion, and the actual generation of the hardware controller. To address combinational explosion, common approaches follow the "divide and conquer" philosophy, producing modular control and/or decentralized control. Most of these approaches do not consider explicit communication between different components of a plant. Synchronization is mostly achieved by sharing of input events, and outputs are abstracted away. We propose an incremental DCS technique which also applies to communicating systems. An initial modular abstraction is followed by a sequence of progressive refinements and computations of approximate control solutions. The last step of this sequence computes an exact controller. This technique is shown to have an improved time/memory efficiency with respect to the traditional global DCS approach. The hardware controller generation addresses the control non-determinism problem in a specific way. A partially closed-loop control architecture is proposed, in order to preserve the applicability of hierarchical design. A systematic technique is proposed and illustrated, for transforming the automatically generated control equation into a vector of control functions. An application of the DCS technique to the correction of certain design errors in a real design is illustrated. To prove the efficiency of the incremental synthesis and controller implementation, a number of examples have been studied.

L'étude des circuits asynchrones est un secteur dans lequel de nombreuses recherches ont été effectuées ces dernières années. Les circuits asynchrones ont démontré plusieurs caractéristiques intéressantes comme la robustesse, l'extensibilité, la faible consommation ou le faible rayonnement électromagnétique. Parmi les différentes classes de circuits asynchrones, les circuits quasi-insensibles aux délais (QDI) ont montré des caractéristiques extrêmement intéressantes en termes de faible consommation et de robustesse aux variations PVT (Process, Voltage, Temperature). L'usage de ces circuits est notamment bien adapté aux applications fonctionnant dans un environnement sévère et pour lesquelles la consommation est un critère primordial. Les travaux de cette thèse s'inscrivent dans ce cadre et visent la conception et la synthèse de machines à états asynchrones (QDI) faiblement consommantes. Une méthode de synthèse dédiée à des contrôleurs asynchrones à faible consommation a donc été développée. Cette technique s'est montrée particulièrement efficace pour synthétiser les contrôleurs de grande taille. La méthode s'appuie sur une modélisation appropriée des contrôleurs et une technique de synthèse dirigée par la syntaxe utilisant des composants spécifiques appelés séquenceurs. Les circuits obtenus ont été vérifiés formellement afin de s'assurer de leurs propriétés en termes de robustesse et de correction fonctionnelle. A cette occasion, une méthode de vérification formelle a été mise en place pour valider les contrôleurs d'une part, et plus généralement, n'importe quel circuit asynchrone d'autre part. Cette technique fait appel à une modélisation hiérarchique des circuits asynchrones en PSL et à un outil de vérification formelle (RAT).

<p>Les travaux de cette thèse s'inscrivent dans le cadre de la validation formelle et le contrôle réactif de calculs à haute performance sur systèmes-sur-puce (SoC). </p> <p>Dans ce contexte, la première contribution est la modélisation synchrone accompagnée d'une transformation d'applications en équations synchrones. Les modéles synchrones permettent de résoudre plusieurs questions liées à la validation formelle via l'usage des outils et techniques formels offerts par la technologie synchrone. Les transformations sont développées selon l'approche d'Ingénierie Dirigé par les Modèles (IDM). </p> <p>La deuxième contribution est une extension et amélioration des mécanismes de contrôle pour les calculs à haute performance, sous forme de constructeurs de langage de haut-niveau et de leur sémantique. Ils ont été défini afin de permettre la vérification, synthèse et génération de code. Il s'agit de déterminer un niveau d'abstraction de représentation des systèmes où soit extraite la partie contrôle, et de la modéliser sous forme d'automates à états finis. Ceci permet de spécifier et implémenter des changements de modes de calculs, qui se distinguent par exemple par les ressources utilisées, la qualité de service fournie, ou le choix d'algorithme remplissant une fonctionnalité. </p> <p>Ces contributions permettent l'utilisation d'outils d'analyse et vérification, tels que la vérification de propriétés d'assignement unique et dépendance acyclique, model checking. L'utilisation de techniques de synthèse de contrôleurs discrets est également traitée. Elles peuvent assurer la correction de faˆ on constructive: à partir d'une spécification partielle du contrôle, la partie manquante pour que les propriétés soient satisfaites est calculée. Grâce à ces techniques, lors du développement de la partie contrôle, la spécification est simplifiée, et le résultat est assuré d'être correct par construction. </p> <p>Les modélisations synchrone et de contrôle reposes sur MARTE et UML. Les travaux de cette thèse sont été partiellement implémentés dans le cadre de Gaspard, dédié aux applications de traitement de données intensives. Une étude de cas est présentée, dans laquelle nous nous intéressont à une application de système embarqué pour téléphone portable multimédia.</p>

Je présente dans ce document mes résultats de recherche sur la conception sûre de systèmes embarqués sûrs. La première partie concerne la répartition automatique de programmes synchrones. Le caractère automatique de la répartition apporte un réel degré de sûreté dans la conception de systèmes répartis car c'est la partie la plus délicate de la spécification qui est automatisée. Grâce à cela, l'absence d'inter-blocage et l'équivalence fonctionnelle entre le programme source centralisé et le programme final réparti peuvent être formellement démontrées. La deuxième partie traite le sujet de l'ordonnancement et de la répartition de graphes de tâches flots-de-données sur des architectures à mémoire répartie, avec contraintes de tolérance aux fautes et de fiabilité. Je présente principalement des heuristiques d'ordonnancement statique multiprocesseur avec pour but la tolérance aux fautes et la fiabilité des systèmes, mais également l'utilisation de méthodes formelles telles que la synthèse de contrôleurs discrets ou les transformations automatiques de programmes. Enfin, la troisième partie concerne les autoroutes automatisées, avec deux volets : la commande longitudinale de véhicules autonomes et les stratégies d'insertion dans les autoroutes automatisées.