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 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.

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.

La conception de systèmes embarqués modernes est de plus en plus complexe, car plus de fonctionnalités sont intégrées dans ces systèmes. En même temps, afin de répondre aux exigences de calcul tout en conservant une consommation d'énergie de faible niveau, MPSoCs sont apparus comme les principales solutions pour tels systèmes embarqués. En outre, les systèmes embarqués sont de plus en plus adaptatifs, comme l’adaptabilité peut apporter un certain nombre d'avantages, tels que la flexibilité du logiciel et l'efficacité énergétique. Cette thèse vise la conception sécuritaire de ces MPSoCs adaptatifs. Tout d'abord, chaque configuration de système doit être analysée en ce qui concerne ses propriétés fonctionnelles et non fonctionnelles. Nous présentons un cadre abstraite de conception et d’analyse qui permet des décisions d’implémentation plus rapide et plus rentable. Ce cadre est conçu comme un support de raisonnement intermédiaire pour les environnements de co-conception de logiciel / matériel au niveau de système. Il peut élaguer l'espace de conception à sa plus grande portée, et identifier les candidats de solutions de conception de manière rapide et efficace. Dans ce cadre, nous utilisons un codage basé sur l’horloge abstrait pour modéliser les comportements du système. Différents scénarios d'applications de mapping et de planification sur MPSoCs sont analysés via les traces d'horloge qui représentent les simulations du système. Les propriétés d'intérêt sont l’exactitude du comportement fonctionnel, la performance temporelle et la consommation d'énergie. Deuxièmement, la gestion de la reconfiguration de MPSoCs adaptatifs doit être abordée. Nous sommes particulièrement intéressés par les MPSoCs implémentés sur des architectures reconfigurables de hardware (ex. FPGA tissus) qui offrent une bonne flexibilité et une efficacité de calcul pour les MPSoCs adaptatifs. Nous proposons un cadre général de conception basésur la technique de la synthèse de contrôleurs discrets (SCD) pour résoudre ce problème. L’avantage principal de cette technique est qu'elle permet une synthèse d'un contrôleur automatique vis-à-vis d’une spécification donnée des objectifs de contrôle. Dans ce cadre, le comportement de reconfiguration du système est modélisé en termes d'automates synchrones en parallèle. Le problème de calcul de la gestion reconfiguration vis-à-vis de multiples objectifs concernant, par exemple, les usages des ressources, la performance et la consommation d’énergie est codé comme un problème de SCD . Le langage de programmation BZR existant et l’outil Sigali sont employés pour effectuer SCD et générer un contrôleur qui satisfait aux exigences du système. Finalement, nous étudions deux façons différentes de combiner les deux cadres de conception proposées pour MPSoCs adaptatifs. Tout d'abord, ils sont combinés pour construire un flot de conception complet pour MPSoCs adaptatifs. Deuxièmement, ils sont combinés pour présenter la façon dont le gestionnaire d'exécution conçu dans le second cadre peut être intégré dans le premier cadre de sorte que les simulations de haut niveau peuvent être effectuées pour évaluer le gestionnaire d'exécution. / The design of modern embedded systems is getting more and more complex, as more func- tionality is integrated into these systems. At the same time, in order to meet the compu- tational requirements while keeping a low level power consumption, MPSoCs have emerged as the main solutions for such embedded systems. Furthermore, embedded systems are be- coming more and more adaptive, as the adaptivity can bring a number of benefits, such as software flexibility and energy efficiency. This thesis targets the safe design of such adaptive MPSoCs. First, each system configuration must be analyzed concerning its functional and non- functional properties. We present an abstract design and analysis framework, which allows for faster and cost-effective implementation decisions. This framework is intended as an intermediate reasoning support for system level software/hardware co-design environments. It can prune the design space at its largest, and identify candidate design solutions in a fast and efficient way. In the framework, we use an abstract clock-based encoding to model system behaviors. Different mapping and scheduling scenarios of applications on MPSoCs are analyzed via clock traces representing system simulations. Among properties of interest are functional behavioral correctness, temporal performance and energy consumption. Second, the reconfiguration management of adaptive MPSoCs must be addressed. We are specially interested in MPSoCs implemented on reconfigurable hardware architectures (i.e., FPGA fabrics), which provide a good flexibility and computational efficiency for adap- tive MPSoCs. We propose a general design framework based on the discrete controller syn- thesis (DCS) technique to address this issue. The main advantage of this technique is that it allows the automatic controller synthesis w.r.t. a given specification of control objectives. In the framework, the system reconfiguration behavior is modeled in terms of synchronous parallel automata. The reconfiguration management computation problem w.r.t. multiple objectives regarding e.g., resource usages, performance and power consumption is encoded as a DCS problem. The existing BZR programming language and Sigali tool are employed to perform DCS and generate a controller that satisfies the system requirements. Finally, we investigate two different ways of combining the two proposed design frame- works for adaptive MPSoCs. Firstly, they are combined to construct a complete design flow for adaptive MPSoCs. Secondly, they are combined to present how the designed run-time manager by the second framework can be integrated into the first framework so that high level simulations can be performed to assess the run-time manager.