De nombreuses techniques ont été développées pour réduire la consommation processeur considéré jusqu'à présent comme l'élément le plus gourmand en consommation. Avec l'évolution technologique et l'apparition de nouvelles applications toujours plus volumineuses en nombre de données, la surface de silicium dédiée aux unités de mémorisation ne cesse de croître. Les techniques d'optimisation ciblant uniquement le processeur peuvent alors être remises en cause avec cette nouvelle tendance. Certaines études montrent que la technique du DVS (Dynamic Voltage Scaling), la plus performante dans la réduction de la consommation processeur, augmente la consommation de la mémoire principale. Cette augmentation est la conséquence d'une part d'une co-activation plus longue de la mémoire avec le processeur et d'autre part de l'augmentation du nombre de préemptions par l'allongement des temps d'exécution des tâches. La solution proposée pour diminuer cet impact négatif du DVS sur la consommation mémoire est de diminuer la surface mémoire co-active. Une architecture mémoire multi-bancs, offrant la possibilité d'activer un seul banc à la fois et de mettre les autres bancs dans un mode faible consommation, est adoptée. Rechercher la configuration mémoire (nombre de bancs, taille de chaque banc) ainsi que l'allocation des tâches aux bancs constitue la contribution majeure de ces travaux. La modélisation de l'énergie consommée par une mémoire multi-bancs a permis d'identifier un nombre important de variables ainsi que leurs fortes dépendances. Cette tendance a rendu le problème difficile à résoudre. Une exploration exhaustive est premièrement développée afin d'évaluer l'impact de chaque paramètre sur la consommation totale de la mémoire. Bien que l'approche exhaustive permette de rendre la solution optimale, l'espace d'exploration augmente exponentiellement avec le nombre de tâches. Ce type de résolution reste intéressant s'il s'agit de l'employer hors ligne sur des applications à faible nombre de tâches. Une heuristique capable d'explorer un sous-espace potentiellement intéressant et de résoudre le problème en un temps polynomial a été développée dans un second temps. La complexité réduite de cette heuristique permet de l'employer en ligne pour effectuer des migrations dans le cas de systèmes à nombre de tâches dynamiques. Des expérimentations sur des applications de traitement de signal temps réel et une application multimédia (GSM et MPEG2) montrent des gains intéressants sur la consommation mémoire. La configuration mémoire obtenue par exploration exhaustive ou par la résolution heuristique couplée à un processeur muni d'une technique de DVFS permet d'augmenter le gain énergétique du système total.

A l'instar d'autres domaines d'activités, l'environnement du marin s'est enrichi d'appareils électroniques à des fins d'aide à la navigation et de sécurité. Dans le cas de la navigation maritime, ces dispositifs ont pour principal but de donner des informations sur l'environnement dans lequel évolue le bateau: profondeur d'eau, bouées de signalisation par exemple et sur son état: cap, vitesse, etc. La complexité et le nombre d'appareils à bord des bateaux dépendent de la taille du bateau, d'un GPS portatif pour un jet-ski à un ensemble complexe d'ECDIS, de radar et d'AIS sur les cargos. Aujourd'hui, malgré l'évolution des appareils d'aide à la navigation, les accidents perdurent (échouage et collisions) et sont en partie dus aux erreurs humaines (33%). Il existe 3 grandes causes:- La charge cognitive trop importante. Cette dernière est liée à la complexité des appareils (ECDIS par exemple) [Jie and Xian-Zhong, 2008], leurs nombres et leurs orientations différentes de la vue pont [Prison and Porathe, 2007].- La mobilité de l'information. La majorité des appareils électroniques à bord des bateaux est positionné à un endroit et ne permet pas l'accès aux données en dehors de cet emplacement.- Le manque de pratique de plaisanciers. Les règles de navigation sont indispensable à la sécurité du marin et peuvent être oubliées par manque de pratique et causent des incidents (ou accidents). Dans ces travaux, nous proposons une solution mobile pour rendre accessible Les données en tout point du bateau. De plus, le prototype est basé sur la technologie de réalité augmentée pour afficher les données dans le champ de vision de l'utilisateur pour une réduction de la charge cognitive. Enfin l'application exécutée sur le prototype délivre uniquement les informations essentielles pour une navigation sécurisée. La première partie de cette thèse détaille une étude utilisateur menée pour comprendre les habitudes et les besoins des plaisanciers afin de sélectionner les données à afficher et leur représentation graphique. Suite à cette étude, une analyse du besoin logiciel et matériel a été menée. Le but de cette analyse est de lister les différents éléments pouvant supporter les contraintes maritimes (soleil, brouillard, nuit, houle, mobilité) afin de proposer un appareil et une application mobile sur technologie de réalité augmentée. La deuxième partie de cette thèse aborde le design du prototype (architecture, display) et du logiciel. Cet ensemble a pour but d'aider le plaisancier lors de conditions météos difficiles. La technologie mise en œuvre dans ce nouvel outil est la réalité augmentée, plus précisément Optical See-through. Le principe de l'application exécutée sur le prototype est un serveur proposant des services à l'utilisateur en fonction des appareils disponibles à bord du bateau tout en limitant la charge cognitive du marin. En effet, l'application conserve uniquement les informations utiles et les affiche dans le champ de vision de l'utilisateur, de plus elles sont superposées à sa vue directe sur le monde.La dernière partie, elle, décrit le générateur de carte qui nous permet d'extraire les données maritimes issues de différents formats de carte pour les adapter au format 3D utilisé dans l'application. Ce dernier est capable de placer automatiquement des objets 3D pour représenter le système de balisage, les amers, etc. Ce générateur a été développé pour reconstituer des zones interdites comme les zones de profondeurs, d'interdiction de chasse sous-marine, etc. Ceci a été mis en œuvre afin de répondre au mieux aux besoins de tous types de plaisanciers, de l'utilisateur de jet-ski au yacht et du pêcheur au plongeur amateur par exemple. / Compared to the other activities, the sailor's environment has been enhanced with electronic devices in order to help the sailor and improve the security. In case of maritime navigation, these devices are mainly used to give information on the environment which the boat moves such as the water depth, seamarks for instance and its state: bearing, speed, etc. The complexity and the number of devices onboard depend on the boat size, from a wearableGPS on a jet-ski to a complex set of ECDIS, radar and AIS on a merchant ship. Today, despite the evolution of the navigational aid devices, the accidents still happen and they are due in part to human errors (33%). There are 3 main causes: The cognitive load issue. The latter is linked to the complexity of devices (ECDIS for instance [Jie and Xian-Zhong, 2008]); their quantity and their orientations which is different from the bridge view or the user's field of view [Prison and Porathe, 2007]. The information's mobility. Most of the devices onboard are put in a specific place and the data are not accessible outside this place. The lack of practice of the recreational boats owner. The maritime navigation rules are vital to sail safely but some of sailors can forget some significations and an accident may result from a wrong choice.In this thesis, we provide a mobile solution to make accessible data everywhere on the boat. Furthermore, the prototype is based on the augmented reality technology to display data in the user's field of view to reduce cognitive load. Finally, the application run on the prototype delivers only the relevant information for a safe navigation. The first part in this thesis details a user study conducted to understand the sailor's habits and their needs in order to select data to display and their graphical representation. Following this study, a needs analysis on the software and hardware has been realized. The purpose of this analysis is to list the different elements that are usable under maritime constraints (sun, fog, night, swell, mobility) in order to provide a device and a mobile application based on the augmented reality technology.The second part in this thesis reaches the prototype (architecture, display) and the software design. Both of them aim to help the sailors when the weather is bad. The technology used in this new tool is the augmented reality, more precisely an Optical see-Through system. The principle of the application run on the prototype is like a server, which provides services to the user depending on devices available onboard, while limiting the sailor's cognitive load. Indeed, the applications keeps only the useful data and display them in the user's field of view, furthermore they are superimposed on his/her direct view of the world.The last part in this thesis details the chart generator, which allows us to extract maritime data from different chart formats to adopt the 3D one used in the application. The latter is able to automate the placement of the 3D objects to build the buoyage system, landmarks, etc. This generator has been developed to recreate the danger areas such as depth areas, prohibited diving areas and so on. This has been done to satisfy user's expectations from the jet-ski to the yacht owner and the fisher man to the diver for instance.

Tableau d’honneur de la Faculté des études supérieures et postdoctorales, 2004-2005 / Ce travail présente une nouvelle technique de compilation dynamique sélective pour les systèmes embarqués avec processeurs ARM. Ce compilateur a été intégré dans la plateforme J2ME/CLDC (Java 2 Micro Edition for Connected Limited Device Con- figuration). L’objectif principal de notre travail est d’obtenir une machine virtuelle accélérée, légère et compacte prête pour l’exécution sur les systèmes embarqués. Cela est atteint par l’implémentation d’un compilateur dynamique sélectif pour l’architecture ARM dans la Kilo machine virtuelle de Sun (KVM). Ce compilateur est appelé Armed E-Bunny. Premièrement, on présente la plateforme Java, le Java 2 Micro Edition(J2ME) pour les systèmes embarqués et les composants de la machine virtuelle Java. Ensuite, on discute les différentes techniques d’accélération pour la machine virtuelle Java et on détaille le principe de la compilation dynamique. Enfin, on illustre l’architecture, le design (la conception), l’implémentation et les résultats expérimentaux de notre compilateur dynamique sélective Armed E-Bunny. La version modifiée de KVM a été portée sur un ordinateur de poche (PDA) et a été testée en utilisant un benchmark standard de J2ME. Les résultats expérimentaux de la performance montrent une accélération de 360 % par rapport à la dernière version de la KVM de Sun avec un espace mémoire additionnel qui n’excède pas 119 kilobytes. / This work presents a new selective dynamic compilation technique targeting ARM 16/32-bit embedded system processors. This compiler is built inside the J2ME/CLDC (Java 2 Micro Edition for Connected Limited Device Configuration) platform. The primary objective of our work is to come up with an efficient, lightweight and low-footprint accelerated Java virtual machine ready to be executed on embedded machines. This is achieved by implementing a selective ARM dynamic compiler called Armed E-Bunny into Sun’s Kilobyte Virtual Machine (KVM). We first present the Java platform, Java 2 Micro Edition (J2ME) for embedded systems and Java virtual machine components. Then, we discuss the different acceleration techniques for Java virtual machine and we detail the principle of dynamic compilation. After that we illustrate the architecture, design, implementation and experimental results of our selective dynamic compiler Armed E-Bunny. The modified KVM is ported on a handheld PDA and is tested using standard J2ME benchmarks. The experimental results on its performance demonstrate that a speedup of 360% over the last version of Sun’s KVM is accomplished with a footprint overhead that does not exceed 119 kilobytes.

Depuis quelques années, on assiste à une expansion fulgurante du marché des terminaux mobiles et sans fil. Dans ce cadre, le déploiement de la technologie Java sur ce type de terminaux connaît un grand succès à cause de ses caractéristiques attrayantes, à savoir la mobilité, la portabilité et la sécurité. En particulier, la plate-forme J2ME/CLDC (Java 2 Micro Edition for Connected Limited Device Configuration) est dédiée au développement d’applications Java qui s’exécutent sur des téléphones cellulaires, des assistants digitaux et de façon générale sur tous les systèmes embarqués dans des appareils électroniques ou industriels. Par ailleurs, la plate-forme J2ME est dotée d’une version allégée de la machine virtuelle Java, appelée KVM (Kilobyte Virtual Machine). Comme toutes machines virtuelles Java, le principal inconvénient de la KVM est sa lenteur d’exécution due au mécanisme d’interprétation. Par conséquent, il y a un besoin réel de disposer de techniques d’accélération qui permettent d’améliorer la performance de la KVM, étant données les contraintes matérielles des plates-formes Java mobiles (ressources mémoire restreintes, puissance de traitement limitée et faible batterie). C’est dans ce contexte particulier que nous abordons la problématique de l’accélération d’une machine virtuelle dédiée à une plate-forme Java mobile. Dans le cadre de cette thèse, nous proposons de concevoir et d’implanter des techniques d’accélération de la machine virtuelle Java pour la plate-forme J2ME/CLDC. Nous proposons également d’élaborer un cadre sémantique pour capturer de manière formelle le langage de bytecode de la plate-forme J2ME/CLDC. Les principaux résultats qui nous ont permis d’atteindre nos objectifs sont : 1. La conception et l’implantation d’un compilateur dynamique sélectif qui accélère la KVM d’un facteur de 400%. également, des techniques accélérant l’appel de méthodes ont été conçues et implantées. 2. élaboration d’un cadre formel dans un style dénotationnel par passage de continuations supportant les aspects intrinsèques du langage Java, à savoir : parallélisme, le non-déterminisme non borné, les structures d’échappement et les données. 3. Spécification du langage de bytecode de la plate-forme J2ME/CLDC dans le cadre sémantique élaboré. / Nowdays, we are witnessing a high expansion of the mobile and wireless devices market. In this context, the Java technology is emerging as a standard execution environment due to its appealing features such as mobility, portability and security. In particular, The J2ME/CLDC platform (Java 2 Micro Edition for Connected Limited Device Configuration) is dedicated to the Java application development for mobile devices and embedded systems. The J2ME/CLDC platform is equipped with a light Java virtual machine, called KVM (Kilobyte Virtual Machine). The main issue of this virtual machine is its performance due to the interpretation mechanism. Consequently, there is a real need to design and implement acceleration techniques for the KVM. Moreover, constraints of wireless and mobile devices in terms of footprint, computation and energy consumption should be considered in the design of these techniques. The main objectives of this thesis are the design and the implementation of acceleration techniques dedicated to the Java virtual machine for the J2ME/CLDC platform. We also intent to elaborate a semantic model to formally capture the bytecode language of the J2ME/CLDC platform.The main research results that achieved these objectives are : 1. The design and implementation of a dynamic selective compiler that speeds up the KVM by a rate of 400%. Other acceleration techniques has been designed and implemented to enhance the method call mechanism. 2. The elaboration of a denotational semantic model with continuations that supports the particular features of the Java language : concurrency, unbounded nondeterminism, escaping constructs and data. 3. The specification of the bytecode language of the J2ME/CLDC platform in the elaborated semantic model.

Tableau d'honneur de la Faculté des études supérieures et postdoctorales, 2006-2007 / With the advent and the rising popularity of wireless Systems, there is a proliferation of small internet-enabled devices (e.g. PDAs, cell phones, pagers, etc.). In this context, Java is emerging as a standard execution environment due to its security, portability, mobility and network support features. In particular, J2ME/CLDC (Java 2 Micro Edition for Connected Limited Device Configuration) is now recognized as the standard Java platform in the domain of mobile wireless devices. An important factor that has amplified the wide industrial adoption of J2ME/CLDC is the broad range of Java based solutions that are available in the market. Ail these factors made Java and J2ME/CLDC an ideal solution for software development in the arena of embedded Systems. A successful deployment of Java on these devices relies on a fast and lightweight execution environment. Our research comes to provide a practical and a theoretical vision about possible solutions to design, implement and validate optimization techniques. More precisely, the research results that led to reach this objective are the following: 1. The design, implementation and evaluation of dynamic acceleration techniques: we have designed and implemented a dynamic selective compiler. This compiler speeds up the execution of embedded Java applications by a rate of 400%. Moreover, we have designed other acceleration techniques for the interpretation and the method call mechanisms. 2. The elaboration of a concurrent denotational semantic model that extends the resource pomsets semantics of Gastin and Mislove with unbounded non-determinism. This model is intended to be accommodated to JVML/CLDC (the bytecode language) and to be used for proving the correctness of the optimizations of JVML/CLDC programs. 3. A case study that shows how this semantic model can be embedded in the proof assistant Isabelle in order to validate optimizations of JVML/CLDC programs. / De nos jours, nous assistons à une croissance fulgurante des réseaux sans fil et des systèmes embarqués (cellulaires, assistants digitaux, etc.). Dans ce contexte, Java a connu une popularité grandissante comme étant un environnement d'exécution standard grâce à ses caractéristiques intrinsèques comme la sécurité, portabilité et mobilité. Plus précisément, J2ME/CLDC (Java 2 Micro Edition for Connected Limited Device Configuration) est devenue une plate-forme standard dans le domaine des systèmes embarqués. En effet, l'important déploiement des téléphones Java a permis une large adoption de cette plate-forme. Le succès de celle-ci nécessite l'existence d'un environnement qui permet une exécution rapide des applications Java. C'est dans ce cadre précis que s'inscrit notre recherche. Notre objectif primordial est de concevoir, implanter et fournir une base formelle pour valider des techniques d'accélération de Java pour les systèmes embarqués. Les principaux résultats ayant contribué à l'atteinte de cet objectif sont les suivants : 1. La conception, l'implantation et l'évaluation d'un compilateur léger et rapide pour l'accélération de l'exécution des applications Java dans les systèmes embarqués. Ce compilateur accélère la machine virtuelle embarquée KVM qui vient avec J2ME/CLDC par un facteur de 4. D'autres techniques d'accélération de l'interprétation et du mécanisme d'appel de méthodes ont été réalisées. 2. L'élaboration d'un modèle sémantique dénotationnel qui étend le modèle resource pomsets de Gastin et Mislove au non-déterminisme non borné. Ce modèle est conçu pour spécifier la sémantique du langage JVML/CLDC (langage bytecode) et aussi pour valider les optimisations de programmes JVML/CLDC. 3. Une étude de cas montrant comment ce modèle peut être embarqué dans l'assistant de preuves Isabelle pour des fins de validation semi-automatique des optimisations de programmes JVML/CLDC.

Le contexte aéronautique a depuis plusieurs années mis en évidence le besoin croissant de technologies de sécurité permettant d'éviter des utilisations malveillantes des matériels ou services installés à bord des avions. La plupart des approches de sécurisation 'avion' se concentre sur des méthodes et techniques permettant de sécuriser les échanges au sein de l'avion. Elles sont cependant inadaptées à la sécurisation dans les cas d'interconnexion des réseaux avioniques avec le reste des réseaux de communication (réseau Internet par exemple). Le problème abordé dans ce travail de thèse vise donc à proposer une architecture de sécurité et de sûreté pour l'ensemble des communications aéronautiques et permettant une interconnexion sécurisée entre le monde 'avion' et le monde extérieur, en tenant compte de l'ensemble des critères de sécurité qui caractérisent les divers environnements traversés et considère dès le départ les divers principes de standardisation associés afin de garantir la pérennité scientifique et industrielle. La solution architecturale proposée dans ce travail de thèse repose principalement sur un composant central de routage, de filtrage et de sécurisation des flux de données aéronautiques. Le travail de conception et de développement de ce composant appelé Routeur Sécurisé de Nouvelle Génération (routeur SNG) a permis une validation expérimentale sur un système reproduisant un système embarqué.

Les systèmes temps-réel critiques sont de plus en plus complexes, et les exigences fonctionnelles et non-fonctionnelles ne cessent plus de croître. Le flot de conception de tels systèmes doit assurer, parmi d’autres propriétés, le déterminisme fonctionnel et la prévisibilité temporelle. Le déterminisme fonctionnel est inhérent aux modèles de calcul flot de données (ex. KPN, SDF, etc.) ; c’est pour cela qu’ils sont largement utilisés pour modéliser les systèmes embarqués de traitement de flux. Un effort considérable a été accompli pour résoudre le problème d’ordonnancement statique périodique et à mémoire de communication bornée des graphes flot de données. Cependant, les systèmes embarqués temps-réel optent de plus en plus pour l’utilisation de systèmes d’exploitation temps-réel et de stratégies d’ordonnancement dynamique pour gérer les tâches et les ressources critiques. Cette thèse aborde le problème d’ordonnancement temps-réel dynamique des graphes flot de données ; ce problème consiste à assigner chaque acteur dans un graphe à une tâche temps-réel périodique (i.e. calcul des périodes, des phases, etc.) de façon à : (1) assurer l’ordonnançabilité des tâches sur une architecture et pour une stratégie d’ordonnancement (ex. RM, EDF) données ; (2) exclure statiquement les exceptions d’overflow et d’underflow sur les buffers de communication ; et (3) optimiser les performances du système (ex. maximisation du débit, minimisation des tailles des buffers). / The ever-increasing functional and nonfunctional requirements in real-time safety-critical embedded systems call for new design flows that solve the specification, validation, and synthesis problems. Ensuring key properties, such as functional determinism and temporal predictability, has been the main objective of many embedded system design models. Dataflow models of computation (such as KPN, SDF, CSDF, etc.) are widely used to model stream-based embedded systems due to their inherent functional determinism. Since the introduction of the (C)SDF model, a considerable effort has been made to solve the static-periodic scheduling problem. Ensuring boundedness and liveness is the essence of the proposed algorithms in addition to optimizing some nonfunctional performance metrics (e.g. buffer minimization, throughput maximization, etc.). However, nowadays real-time embedded systems are so complex that real-time operating systems are used to manage hardware resources and host real-time tasks. Most of real-time operating systems rely on priority-driven scheduling algorithms (e.g. RM, EDF, etc.) instead of static schedules which are inflexible and difficult to maintain. This thesis addresses the real-time scheduling problem of dataflow graph specifications; i.e. transformation of the dataflow specification to a set of independent real-time tasks w.r.t. a given priority-driven scheduling policy such that the following properties are satisfied: (1) channels are bounded and overflow/underflow-free; (2) the task set is schedulable on a given uniprocessor (or multiprocessor) architecture. This problem requires the synthesis of scheduling parameters (e.g. periods, priorities, processor allocation, etc.) and channel capacities. Furthermore, the thesis considers two performance optimization problems: buffer minimization and throughput maximization.

Nowadays, computer systems are everywhere. From simple portable devices such as watches and MP3 players to large stationary installations that control nuclear power plants, computer systems are now present in all aspects of our modern and every-day life. In about only 70 years, they have completely perturbed our way of life and they reached a so high degree of sophistication that they will be soon capable of driving our cars and cleaning our houses without any human intervention. As computer systems gain in responsibilities, it becomes essential that they provide both safety and reliability. Indeed, a failure in systems such as the anti-lock braking system (ABS) in cars could threaten human lives and generate catastrophic and irreversible consequences. Hence, for many years, researchers have addressed these emerging problems of system safety and reliability which come along with this fulgurant evolution. <p><p>This thesis provides a general overview of embedded real-time computer systems, i.e. a particular kind of computer system whose number grows daily. We provide the reader with some preliminary knowledge and a good understanding of the concepts that underlie this emerging technology. We focus especially on the theoretical problems related to the real-time issue and briefly summarizes the main solutions, together with their advantages and drawbacks. This brings the reader through all the conceptual layers constituting a computer system, from the software level---the logical part---that specifies both the system behavior and requirements to the hardware level---the physical part---that actually performs the expected treatments and reacts to the environment. In the meanwhile, we introduce the theoretical models that allow researchers for theoretical analyses which ensure that all the system requirements are fulfilled. Finally, we address the energy consumption problem in embedded systems. We describe the various factors of power dissipation in modern technologies and we introduce different solutions to reduce this consumption./Cette thèse se focalise sur un type de systèmes informatiques bien précis appelés “systèmes embarqués temps réel”. Un système est dit “embarqué” lorsqu’il est développé afin de servir un but bien précis. Un téléphone portable est un parfait exemple de système embarqué étant donné que toutes ses fonctionnalités sont rigoureusement définies avant même sa conception. Au contraire, un ordinateur personnel n’est généralement pas considéré comme un système embarqué, les concepteurs ne sachant pas à l’avance à quelles fins il sera utilisé. Une grande partie de ces systèmes embarqués ont des contraintes temporelles très fortes, ce qui les distingue encore plus des ordinateurs grand public. A titre d’exemple, lorsqu’un conducteur de voiture freine brusquement, l’ordinateur de bord déclenche l’application ABS et il est primordial que cette application soit traitée endéans une courte échéance. Autrement dit, cette fonctionnalité ABS doit être traitée prioritairement par rapport aux autres fonctionnalités du véhicule. Ce type de système embarqué est alors dit “temps réel”, dû à ces notions de temps et de priorités entre les applications. La problèmatique posée par les systèmes temps réel est la suivante. Comment déterminer, à tout moment, un ordre d’exécution des différentes fonctionnalités de telle sorte qu’elles soient toutes exécutées entièrement endéans leur échéance ?De plus, avec l’apparition récente des systèmes multiprocesseurs, cette problématique s’est fortement complexifiée, vu que le système doit à présent déterminer quelle fonctionnalité s’exécute à quel moment sur quel processeur afin que toutes les contraintes temporelles soient respectées. Pour finir, ces systèmes embarqués temp réel multiprocesseurs se sont rapidement retrouvés confrontés à un problème de consommation d’énergie. Leur demande en terme de performance (et donc en terme d’énergie) à évolué beaucoup plus rapidement que la capacité des batteries qui les alimentent. Ce problème est actuellement rencontré par de nombreux systèmes, tels que les téléphones portables par exemple. L’objectif de cette thèse est de parcourir les différents composants de tels système embarqués et de proposer des solutions afin de réduire leur consommation d’énergie. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Ces cinquante dernières annéees, les ordinateurs ont occupé une place toujours plus importante dans notre vie quotidienne. On les retrouve aujourd’hui présents dans de nombreuses applications, sous forme de systèmes enfouis. Ces applications sont parfois critiques, dans la mesure où toute défaillance du système informatique peut avoir des conséquences catastrophiques, tant sur le plan humain que sur le plan économique. <p>Nous pensons par exemple aux systèmes informatiques qui contrôlent les appareils médicaux ou certains systèmes vitaux (comme les freins) des véhicules automobiles. <p>Afin d’assurer la correction de ces systèmes informatiques, différentes techniques de vérification Assistée par Ordinateur ont été proposées, durant les trois dernières <p>décennies principalement. Ces techniques reposent sur un principe commun: donner une description formelle tant du système que de la propriété qu’il doit respecter, et appliquer une méthode automatique pour prouver que le système respecte la propriété. <p>Parmi les principaux modèles aptes à décrire formellement des systèmes informatiques, la classe des systèmes de transition bien structurés [ACJT96, FS01] occupe une place importante, et ce, pour deux raisons essentielles. Tout d’abord, cette classe généralise plusieurs autres classes bien étudiées et utiles de modèles à espace <p>d’états infini, comme les réseaux de Petri [Pet62](et leurs extensions monotones [Cia94, FGRVB06]) ou les systèmes communiquant par canaux FIFO avec pertes [AJ93]. Ensuite, des problèmes intéressants peuvent être résolus algorithmiquement sur cette classe. Parmi ces problèmes, on trouve le probléme de couverture, auquel certaines propriétés intéressantes de sûreté peuvent être réduites. <p>Dans la première partie de cette thèse, nous nous intéressons au problème de couverture. Jusqu’à présent, le seul algorithme général (c’est-à-dire applicable à n’importe quel système bien structuré) pour résoudre ce problème était un algorithme dit en arrière [ACJT96] car il calcule itérativement tous les états potentiellement non-sûrs et vérifie si l’état initial du système en fait partie. Nous proposons Expand, Enlarge and Check, le premier algorithme en avant pour résoudre le problème de couverture, qui calcule les états potentiellement accessibles du système et vérifie si certains d’entre eux sont non-sûrs. Cette approche est plus efficace en pratique, comme le montrent nos expériences. Nous présentons également des techniques permettant d’accroître l’efficacité de notre méthode dans le cas où nous analysons des réseaux de Petri (ou <p>une de leurs extensions monotones), ou bien des systèmes communiquant par canaux FIFO avec pertes. Enfin, nous nous intéressons au calcul de l’ensemble de couverture pour les réseaux de Petri, un objet mathématique permettant notamment de résoudre le problème de couverture. Nous étudions l’algorithme de Karp & Miller [KM69], une solution classique pour calculer cet ensemble. Nous montrons qu’une optimisation de cet algorithme présenté dans [Fin91] est fausse, et nous proposons une autre solution totalement neuve, et plus efficace que la solution de Karp & Miller. <p>Dans la seconde partie de la thèse, nous nous intéressons aux pouvoirs d’expression des systèmes bien structurés, tant en terme de mots infinis que de mots finis. Le pouvoir d’expression d’une classe de systèmes est, en quelque sorte, une mesure de la diversité des comportements que les modèles de cette classe peuvent représenter. En ce qui concerne les mots infinis, nous étudions les pouvoirs d’expression des réseaux de Petri et de deux de leurs extensions (les réseaux de Petri avec arcs non-bloquants et les réseaux de Petri avec arcs de transfert). Nous montrons qu’il existe une hiérarchie stricte entre ces différents pouvoirs d’expression. Nous obtenons également des résultats partiels concernant le pouvoir d’expression des réseaux de Petri avec arcs de réinitialisation. En ce qui concerne les mots finis, nous introduisons la classe des langages bien structurés, qui sont des langages acceptés par des systèmes de transition bien structurés étiquettés, où l’ensemble des états accepteurs est clos par le haut. Nous prouvons trois lemmes de pompage concernant ces langages. Ceux-ci nous permettent de réobtenir facilement des résultats classiques de la littérature, ainsi que plusieurs nouveaux résultats. En particulier, nous prouvons, comme dans le cas des mots infinis, qu’il existe une hiérarchie stricte entre les pouvoirs d’expression des extensions des réseaux de Petri considérées. / Doctorat en sciences, Spécialisation Informatique / info:eu-repo/semantics/nonPublished

<p align="justify">Computer Science is currently facing a grand challenge :finding good design practices for embedded systems. Embedded systems are essentially computers interacting with some physical process. You could find one in a braking systems or in a nuclear power plant for example. They present several design difficulties :first they are reactive systems, interacting indefinitely with their environment. Second,they must satisfy real-time constraints specifying when they should respond, and not only how. Finally, their environment is often deeply continuous, presenting complex dynamics. The formal models of choice for specifying such systems are timed and hybrid automata for which model checking is pretty well studied.</p> <p><p align="justify">In a first part of this thesis, we study a complete design approach, including verification and code generation, for timed automata. We have to define a new semantics for timed automata, the AASAP semantics, that preserves the decidability properties for model checking and at the same time is implementable. Our notion of implementability is completely novel, and relies on the simulation of a semantics that is obviously implementable on a real platform. We wrote tools for the analysis and code generation and exemplify them on a case study about the well known Philips Audio Control Protocol.</p> <p><p align="justify">In a second part of this thesis, we study the problem of controller synthesis for an environment specified as a hybrid automaton. We give a new solution for discrete controllers having only an imperfect information about the state of the system. In the process, we defined a new algorithm, based on the monotonicity of the controllable predecessors operator, for efficiently finding a controller and we show some promising applications on a classical problem :the universality test for finite automata. / Doctorat en sciences, Spécialisation Informatique / info:eu-repo/semantics/nonPublished