La mémoire est considérée comme étant gloutonne en consommation d'énergie, un problème sensible, particulièrement dans les systèmes embarqués. L'optimisation globale de fonctions multimodales est également un problème délicat à résoudre du fait de la grande quantité d'optima locaux de ces fonctions. Dans ce mémoire, je présente différents nouveaux algorithmes hybrides et distribués afin de résoudre ces deux problèmes d'optimisation. Ces algorithmes sont comparés avec les méthodes classiques utilisées dans la littérature et les résultats obtenus sont encourageants. En effet, ces résultats montrent une réduction de la consommation d'énergie en mémoire d'environ 76% jusqu'à plus de 98% sur nos programmes tests, d'une part. D'autre part, dans le cas de l'optimisation globale de fonctions multimodales, nos algorithmes hybrides convergent plus souvent vers la solution optimale globale. Des versions distribuées et coopératives de ces nouveaux algorithmes hybrides sont également proposées. Elles sont, par ailleurs, plus rapides que leurs versions séquentielles respectives. / Résumé en anglais : Memory is considered to be greedy in energy consumption, a sensitive issue, especially in embedded systems. The global optimization of multimodal functions is also a difficult problem because of the large number of local optima of these functions. In this thesis report, I present various new hybrid and distributed algorithms to solve these two optimization problems. These algorithms are compared with conventional methods used in the literature and the results obtained are encouraging. Indeed, these results show a reduction in memory energy consumption by about 76% to more than 98% on our benchmarks on one hand. On the other hand, in the case of global optimization of multimodal functions, our hybrid algorithms converge more often to the global optimum solution. Distributed and cooperative versions of these new hybrid algorithms are also proposed. They are more faster than their respective sequential versions.

Les systèmes embarqués sont largement utilisés de nos jours. Pour des raisons d'efficacité, les plus contraints en termes de ressources sont toujours programmés en C et en assembleur. L'adoption de langages de plus haut niveau tels que C# ou Java offrirait plus d'abstraction au programmeur, ce qui réduirait les temps de développement et par conséquent le coût de ces systèmes. Certains d'entre eux ont déjà migré vers de tels langages, comme les téléphones mobiles ou les tablettes tactiles, mais ils sont équipés d'une grande quantité de mémoire externe et ne reflètent pas la majorité des systèmes embarqués.Cette thèse s'intéresse à l'implémentation de Java et .NET pour l'embarqué, et plus spécifiquement à la compilation efficace du polymorphisme. Ce polymorphisme génère un certain coût à l'exécution, comme des indirections dans le cas des appels de méthodes (polymorphisme d'inclusion), ou de la duplication de code dans le cas de la généricité (polymorphisme paramétrique). De nombreuses techniques d'implémentation ont été proposées, notamment pour Java. Il reste cependant à identifier lesquelles sont applicables pour le type de systèmes que nous ciblons, et à en concevoir de nouvelles pour certains aspects comme la généricité. Nous partons du principe que les techniques globales (hypothèse du monde clos) sont les mieux adaptées. Par l'analyse de types, nous détectons qu'une partie importante des programmes est monomorphe et qu'elle peut donc être compilée sans surcoût. Pour implémenter le polymorphisme restant, nous choisissons la technique la mieux adaptée au matériel cible. Nous proposons également une implémentation de la généricité qui est adaptée aux systèmes embarqués. D'après nos évaluations, l'impact négatif du polymorphisme sur l'efficacité est largement réduit. L'efficacité du code optimisé devrait s'approcher de celle du C, et les techniques que nous employons pourraient être applicables dans le contexte plus général du chargement dynamique. / Nowadays, embedded systems are ubiquitous. For efficiency reasons, most constrained systems are still programmed in C and assembly. Adopting higher-level languages such as C# or Java should enhance the level of abstraction offered to programmers and reduce development time and cost for these systems. A small part of them have migrated to such languages, like smartphones and tablet computers, but they have a large amount of external memory available and do not represent the majority of embedded systems.This thesis focuses on the implementation of Java and .NET for embedded systems, and more especially on the efficient compilation of polymorphism. Polymorphism generates an overhead at run-time, such as indirections when methods are invoked (inclusion polymorphism) or code duplication in the case of generics (parametric polymorphism). Many implementation techniques have been proposed, especially for Java. However, it remains to identify which ones are applicable in the context of low-end embedded systems. We consider that whole program optimization (closed-world assumption) is well-suited in this context. Using type analysis, we observe that most part of programs is monomorph, therefore it can be compiled with no overhead with respect to C. In order to implement the remaining polymorphism, we choose the technique which is better suited for the target hardware. We also propose an appropriate implementation of run-time generics. Our results show that the negative impact of polymorphism is mostly reduced. The efficiency of the optimized code should be comparable with C, and the techniques we employ could be applicable in the context of dynamic loading (open-world assumption).

L'augmentation du nombre de systèmes interconnectés et l’expansion des données échangées dans les réseaux avioniques ont contribué à la complexification des architectures de communication. Pour gérer cette évolution, une nouvelle solution basée sur un réseau cœur haut débit, e.g., l'AFDX (Avionics Full DupleX), a été implémentée sur l'A380. Cependant, il reste des réseaux bas débit, e.g, CAN ou A429, utilisés pour certaines fonctions spécifiques. Cette architecture réduit le délai de développement, mais en contrepartie, elle conduit à de l’hétérogénéité et à de nouveaux challenges pour garantir les contraintes temps-réel. Pour résoudre ces challenges, une architecture homogène basé sur l'AFDX pourrait apporter de grands avantages, tels que une facilité de l'installation et maintenance, et une réduction de poids et coûts. Cette architecture homogène doit supporter des applications de criticités mixtes, où coexistent les trafics critiques (SCT), Best-effort (BE) et le trafic AFDX actuel (RC). Pour atteindre ce but, nous commençons par évaluer les avantages et les inconvénients des solutions existantes par rapport aux contraintes avioniques. Cela nous conduit à sélectionner le Burst Limiting Shaper (BLS) (proposé par le groupe IEEE Time Sensitive Networking (TSN)) allié à un ordonnanceur Static Priority non-preemptif. Ainsi, nous identifions quatre contributions principales dans cette thèse. Tout d'abord, nous spécifions un AFDX étendu avec le TSN/BLS. Une analyse préliminaire basée sur de la simulation a donné des résultats encourageants pour poursuivre sur cette voie. En second, nous détaillons une analyse temporelle de l'AFDX étendu, grâce au Network Calculus, pour calculer des bornes maximales des délais pire cas des différents types de trafic, pour prouver le déterminisme du réseau et le respect des contraintes temporelles. Une analyse de performance préliminaire montre l'efficacité de la solution à améliorer les délais de RC, tout en garantissant les contraintes. Cependant, cette analyse a aussi montré certaines limitations du modèle en termes de pessimisme. Notre troisième contribution est par conséquent la réduction de ce pessimisme, grâce à une seconde modélisation de l'AFDX étendu, et à une méthode de paramétrage des variables système. Cette méthode permet d'améliorer les performances de RC tout en garantissant les contraintes temporelles du SCT et RC. Finalement, nous validons notre proposition à travers des études de cas avioniques réalistes pour vérifier son efficacité. Les résultats montrent une forte amélioration des délais de RC ainsi que de l'ordonnançabilité de SCT et RC, en comparaison à l'AFDX actuel et au Deficit Round Robin. / The growing number of interconnected end-systems and the expansion of exchanged data in avionics have led to an increase in complexity of the communication architecture. To cope with this trend, a first communication solution based on a high rate backbone network, i.e., the AFDX (Avionics Full Duplex Switched Ethernet), has been implemented by Airbus in the A380. Moreover, some low rate data buses, e.g., CAN or ARINC 429, are still used to handle some specific avionics domains. Although this architecture reduces the time to market, it conjointly leads to inherent heterogeneity and new challenges to guarantee the real-time requirements. To handle these emerging issues, a homogeneous avionic communication architecture based the AFDX technology to interconnect different avionics domains may bring significant advantages, such as easier installation and maintenance and reduced weight and costs. Furthermore, this homogeneous communication architecture needs to support mixed-criticality applications, where safety-critical traffic (SCT), current rate constraint AFDX traffic (RC) and best effort traffic (BE) co-exist. To achieve this aim, first, we assess the pros and cons of most relevant existing solutions vs the main avionics requirements, to support mixed-criticality applications on the AFDX network. Afterwards, the Burst Limiting Shaper (BLS) (proposed by IEEE Time Sensitive Networking (TSN) Task group) on top of a Non-Preemptive Static Priority (NP-SP) scheduler has been selected as the most promising solution. Hence, our main contributions in this thesis are fourfold. First, we specify the extended AFDX incorporating the TSN/BLS on top of NP-SP. A preliminary performance analysis based on simulations has been conducted. These first results were encouraging to pursue this proposal. Second, we conduct a timing analysis of the extended AFDX using Network Calculus to compute the delay upper bounds of the different traffic classes and prove the determinism of such a solution. The preliminary performance evaluation has shown the efficiency of the extended AFDX to enhance the RC delay bounds while guaranteeing the constraints. However, they have also highlighted some limitations of the proposed model in terms of pessimism. Third, we introduce a second model of the extended AFDX to enhance the delay bounds tightness. Moreover, we propose a tuning method of TSN/BLS parameters to enhance as much as possible the RC timing performance, while guaranteeing the constraints. Finally, we validate our proposal through representative case studies to assess its efficiency. The results show the enhancements of the RC delay bounds as well as the schedulability level of both SCT and RC traffic, in comparison to the current AFDX and Deficit Round Robin (DRR).

L’accroissement continu de la complexité des systèmes embarqués pose un problème majeur pour leur développement lequel doit aussi prendre en compte les exigences extra-fonctionnelles et les contraintes du domaine telles que la limitation et le partage des ressources, la distribution, et les contraintes temporelles et de fiabilité. De ce fait, les systèmes embarqués requièrent de nouvelles solutions pouvant efficacement et de manière prévisible répondre à l’ensemble de ces besoins. L’ingénierie logicielle basée composants est un paradigme qui a déjà démontré des aptitudes pour appréhender la complexité logicielle. Cependant, pour supporter de manière efficace les propriétés extra-fonctionnelles, un modèle de composants doit posséder des mécanismes spécifiques. L’objectif de cette thèse est de construire un tel support. Pour ce faire, nous avons analysé de manière systématique des modèles de composants existants à ce jour et identifié des challenges relatifs à la réalisation d’une approche basée composants dédiée au développement des systèmes embarqués. S’appuyant sur ces challenges, nous avons avancé l’état de l’art en développant ProCom, un nouveau modèle de composants qui répond aux attentes des systèmes embarqués au travers de sa sémantique d’exécution et de sa structuration en niveaux. Centré autour de ProCom, nous avons aussi développé PRIDE, son environnement de développement intégré. PRIDE couvre le procédé de développement des premières phases de spécification jusqu’à la synthèse et le déploiement et fournit des moyens d’intégrer différents outils d’analyse et de vérification. La contribution principale de cette thèse réside dans la modélisation et la réalisation d’un support pour la gestion des propriétés extra-fonctionnelles pour les systèmes embarqués construits à base de composants logiciels. Ce support facilite la spécification, le management et l’intégration de propriétés multi-valuées tenant compte du contexte dans lequel elles ont été établies. Les propriétés peuvent être attachées aux éléments architecturaux des modèles de composants et leurs valeurs peuvent être comparées et raffinées durant le développement. En particulier, le fait d’avoir des valeurs multiples avec leur contexte d’évaluation permet de comparer des valeurs provenant de différentes sources. Les concepts proposés ont été illustrés au travers d’exemples représentatifs de systèmes. / The continuously increasing complexity of embedded systems is a major issue for their development, which, in addition, must also consider specific extra-functional requirements and constraints, such as limited and shared resources, distribution, timing, and dependability. Thus, embedded systems call for development solutions that can efficiently and predictably cope with these issues. Component-based software engineering is a proven paradigm to handle complexity. Yet, for efficiently managing extra-functional properties, a component model needs to have dedicated mechanisms that provide a suitable support for their management. The objective of this thesis is to build this support. We have performed a systematic analysis of existing component models and identified challenges of applying a component-based approach to embedded system development. Based on these challenges we have advanced the current state-of-the-art by developing a new component model, called ProCom, that accommodates the specifics of embedded systems through its well-defined execution semantics and layered structure. Centered around ProCom, we have also developed PRIDE, the ProCom Integrated Development Environment. PRIDE supports the development from early specification to synthesis and deployment, providing the means to aggregate various analysis and verification tools. The main contribution of the thesis is in the design and implementation of an extra-functional property management framework that enables to seamlessly specify, manage and integrate multi-valued context-aware extra-functional properties of component-based embedded systems. Properties can be attached to architectural elements of component models and their values can be compared and refined during the development process. In particular, having multiple context-aware values allows values from different sources to be compared. The proposed concepts have been demonstrated on several representative example systems.

De manière générale, les turbomachines sont des machines tournantes permettant la conversion des différents types d’énergie. Ces dernières sont composées d’une partie mécanique en rotation, appelée rotor, interagissant avec un fluide. La rotation a donc un rôle clé pour ces machines et la liaison entre les parties fixes et les parties tournantes, appelée palier, est primordiale pour un fonctionnement fiable et optimal. Les turbomachines supportées par des paliers magnétiques actifs (PMAs) sont de plus en plus utilisées par les industriels notamment grâce à l’absence de contact direct entre parties fixes et parties tournantes, permettant un gain d’énergie et une réduction des émissions de CO2. La plupart du temps, ces machines sont « embarquées » et reposent sur des supports mobiles. Les mouvements générés par ces supports doivent être considérés dans la prévision du comportement dynamique des turbomachines afin d’améliorer les designs en conséquence. Cette thèse est une contribution à l’étude des turbomachines supportées par des PMAs sujettes à de fortes sollicitations extérieures. L’approche est numérique et expérimentale. L’utilisation d’un banc d’essais académique composé d’un système rotor-PMA, aux propriétés d’une turbomachine industrielle, a permis de tester les modèles développés pour des cas de sollicitations extérieures de type séisme et choc, générées grâce à l'excitateur 6-axes de l'equipex PHARE. Il est montré que le modèle permet la bonne prévision du comportement réel de la machine. Cet outil pourra donc être utilisé pour des designs de type industriel. / Turbomachines are rotating machines enabling the conversion of the different types of energy. The latter are composed of a rotating mechanical part, called rotor, interacting with a fluid. Therefore, rotation play a key role in these machines and the mechanical link between the fixed and the rotating parts, called bearing, is essential for reliable and optimal operations. Turbomachines supported by active magnetic bearings (AMBs) are increasingly used by industrial companies, especially thanks to the absence of direct contact between fixed and rotating parts, enabling energy savings and reduction of CO2 emissions. Most of the time, these machines are "on-board" and are fixed on mobile supports. The motions generated by these supports must be considered in the prediction of the dynamic behaviour of turbomachinery in order to improve the designs accordingly. This PhD is a contribution to the study of turbomachines supported by AMBs subjected to strong external base motions. The approach is numerical and experimental. The use of an academic scale test rig comprising a rotor-AMB system, with the properties of an industrial turbomachine, allowed to test the developed models for cases of external solicitations such as earthquake and shock, thanks to the 6-axis shaker of the equipex PHARE. It is shown that the model provides good predictions of the behaviour of the machine for the tested cases. This tool can therefore be used for industrial designs.

Les véhicules électriques présentent désormais une alternative crédible aux véhicules équipés demoteurs à combustion interne. Ils sont plus propres et plus confortables à l’utilisation. La gestion del’énergie d’un véhicule électrique est actuellement focalisée sur le fonctionnement du moteur, principalconsommateur d’énergie, sans tenir compte du confort de l’utilisateur.Le travail présenté dans cette thèse intègre la prise en compte des préférences utilisateur au seinde la gestion de l’énergie des véhicules électriques. La contribution est réalisée par un canevas logicielnommé ORQA. Dans un premier temps, les organes du véhicule sont caractérisés par leurs besoinsénergétiques et par les niveaux de qualité de service qu’ils proposent. Un gestionnaire d’énergie estensuite intégré au système logiciel du véhicule. Il se base sur les caractéristiques des organes et propose àl’utilisateur une solution de configuration de trajet prenant en compte ses préférences d’utilisation ainsique d’éventuelles contraintes de temps et d’énergie. Cette solution définit des contraintes d’utilisationsur le moteur et les organes de confort lors du déroulement du trajet.Le gestionnaire d’énergie est exécuté au sein des systèmes embarqués du véhicule dont les platesformessont fortement contraintes. Pour satisfaire celles-ci, il est primordial de proposer une configurationefficace du gestionnaire d’énergie. L’intérêt et la validité de l’approche employée sont démontrésau travers de la comparaison entre la configuration originelle et une configuration optimisée sur deuxvéhicules exemples. / Electric vehicles are nowadays a viable alternative to vehicles built around an internal combustionengine. They offer a cleaner and more comfortable driving thanks to the electric engine. The energymanagement of an electric vehicle is usually focused on the engine operation, the biggest energyconsumer, thus ignoring the user comfort.The contribution presented in this thesis allows for the consideration of the user preferences insidethe energy management of electric vehicles. It takes shape with a framework named ORQA. First,the vehicle devices are characterised by their energy requirements and the quality levels they offer.An energy manager based on the devices characteristics is then integrated into the software systemof the vehicle. The manager offers the user a solution to configure a trip request. The configuration isbased on the usage preferences and optional constraints over duration and consumption. The solutiondefines a set of constraints on the motor and on the comfort-related devices during the trip execution.The energy manager is executed in the embedded systems of the vehicle which platforms are highlyconstrained. Thus, the energy manager’s implementation is optimised to satisfy the execution platformconstraints. The interest and the validity of the chosen approach are attested by the comparison ofthe original configuration and an optimised configuration on two example vehicles.

Aujourd'hui, les systèmes embarqués sont de plus en plus utilisés pour contrôler les systèmes complexes. Dans ce travail de thèse, nous nous intéressons aux systèmes embarqués critiques utilisés pour la commande de systèmes de transport comme les systèmes ferroviaires. Le but de ce travail est de permettre la conception de systèmes tolérants aux fautes pour le contrôle-commande des systèmes de transport. Nous proposons une nouvelle approche de modélisation des systèmes embarqués temporisés pour le diagnostic de leurs fautes. Elle est basée sur une décomposition structurelle du système et sur une extension de la diagnosticabilité modulaire au contexte des systèmes temporisés. On distingue deux approches de base pour le diagnostic de fautes des SED, une approche basée sur les diagnostiqueurs et une approche basée sur les signatures temporelles causales (STC). La principale limite de l’approche diagnostiqueur réside dans la gestion de l’explosion combinatoire. Dans ce travail, notre verrou principal est de combattre cette limite. Nous proposons une nouvelle méthode basée sur l’ingénierie par les modèles pour le diagnostic des systèmes embarqués critiques. D’autre part, la limite majeure de l’approche STC est la garantie de la cohérence d’une base de STC. Un deuxième niveau de difficulté réside dans l’interprétation des événements en entrée du système de diagnostic dans le cadre de l’hypothèse de défaillances multiples. Dans ce travail, nous proposons deux méthodes différentes pour la vérification de la cohérence d’une base de STC et nous proposons un algorithme d’interprétation basé sur le concept de monde qui garantit la correction du diagnostic / Today, embedded systems are increasingly used to control complex systems. In this thesis, we are interested in critical embedded systems used for the control of transport systems such as railway systems. The aim of this work is to enable the design of fault-tolerant systems for the control of transport systems. We propose a new timed embedded systems modeling approach to diagnose their faults. It is based on decomposition of the system and structural extension of diagnosability context of modular timed systems. In DES, there are two basic approaches for diagnosis: diagnoser based approach and chronicles (Causal Temporal Signature (CTS)) based approach. The major limitation of diagnoser approaches rely in the management of the combinatorial explosion related to the formalism of automata. In this work, our main lock is to combat this limit. We propose new engineering models based method for the diagnosis of critical embedded systems. On the other hand, the major limitation of chronicles approach is first to be able to guaranty the consistency of a database. A second level of difficulty is in interpreting some sequences of events at the input of the diagnostic system under the hypothesis of multiple failures. In this work, we propose two different methods to verify the consistency of a set of CTS and we propose an interpretation algorithm based on a concept of worlds which guarantees the correct diagnosis

L'intérêt de la communauté de la sécurité numérique dans le domaine des Systems on Chip (SoC) s'est essentiellement focalisé sur les menaces logicielles, améliorant sans cesse le niveau de protection. Cependant, l'exploitation de ce vecteur d'attaque devenant de plus en plus difficile, il est fort probable que les attaques matérielles se multiplient. Par conséquent, il est primordial d'étudier ces dernières afin d'anticiper la menace qu'elles représentent. La sophistication de l'architecture et la rapidité d'évolution des technologies embarquées dans les SoC, justifient la mise en place d'une méthodologie adaptée pour évaluer efficacement leur niveau de sécurité. C'est dans ce contexte que cette thèse propose l'étude de cette catégorie d'attaques ainsi qu'un aperçu de leur impact sur la sécurité de ce type de systèmes. Alors que les architectures élaborées accroissent la difficulté de mise en place d'attaques physiques, elles augmentent également la surface d'attaque. Une première étude analyse les chemins d'attaques afin de déterminer les grandeurs physiques exploitables les plus pertinentes. Cette étape conduit, dans un deuxième temps, à l'élaboration de règles génériques pour l'évaluation sécuritaire des SoC présents sur le marché. Celles-ci combinent diverses techniques déjà utilisées dans le domaine de la carte à puce. L'ensemble de ce travail s'appuie sur plusieurs divers modules caractéristiques de la sécurité des SoC actuels. Tous les résultats soulignent que la complexité inhérente aux SoC n'est pas suffisante pour les protéger contre les attaques matérielles et l'implémentation des sécurités dans ces systèmes doit se faire sans se reposer sur cette propriété. / In the field of System on Chip (SoC), the digital security community has mainly focused on software threats; constantly working to improve the level of protection. Since the exploitation of this attack vector is becoming more and more difficult, it is most likely that the number of hardware attacks will increase. Therefore, it is essential to study these attacks in order to anticipate the threat they represent. The sophisticated architecture and the rapidly changing technologies embedded in the SoC justify the implementation of an adapted methodology, to effectively evaluate their level of security.In this context, this thesis examines the feasibility of this type of attacks and their impact on the security of these systems. While rich architectures increase the difficulty of setting up hardware attacks, they also increase the attack surface. Our study starts by analyzing the attack paths in order to determine the most relevant exploitable physical quantities. This has led to the development of a generic procedure for the security evaluation of SoCs on the market. This method combines various techniques that are already applied to smart cards. This entire work is based on several case studies related to various embedded modules characteristic of the security in current systems-on-chips. All the observed results lead to the same observations: the inherent complexity of SoCs is not sufficient to protect them against hardware attacks. The implementation of security in these systems must be done without relying on this property.

Bien que de nombreux appareils numériques soient aujourd'hui capables de lire des contenus vidéo en temps réel et d'offrir une restitution de grande qualité, le décodage vidéo dans les systèmes embarqués n'en est pas pour autant devenu une opération anodine. En effet, les codecs récents tels que H.264 et HEVC sont d'une complexité telle que le recours à des architectures mixtes logiciel/matériel est presque incontournable. Or les plateformes de ce type sont notoirement difficiles à programmer efficacement. Cette thèse relève le défi du développement d'applications à flux de données pour les cibles embarquées hybrides et de leur exécution efficace, et propose plusieurs contributions. La première est une extension des heuristiques d'ordonnancement de liste pour tenir compte des contraintes mémorielles. La seconde est un modèle d'exécution à flot de données compatible avec la plupart des modèles existants et avec une large classe de plateformes matérielles, ainsi qu'un ordonnanceur dynamique. Enfin, de nombreux développements ont été menés sur une architecture réelle de STMicroelectronics pour démontrer la faisabilité de l'approche. / Although numerous electronic devices are nowadays able to play video contents in real time and offer high-quality reproduction, video decoding in embedded systems has not become a trivial process yet. As a mater of fact, recent codecs such as H.264 and HEVC exhibit such a complexity that resorting to mixed sofware-hardware architecture is almost unavoidable. However, programming efficiently this kind of platforms is well-known to be tricky. This thesis addresses the issue of developing streaming applications for hybrid embedded targets and executing them efficiently, and proposes several contributions. The first one is an extension of the classical list-scheduling heuristics to take memory constraints into account. Te second one is a datafow execution model compatible with most existing models and with a large set of hardware platforms, as well as a dynamic scheduler. Lastly, numerous developments have been carried out on a real-world architecture from STMicroelectronics so as to demonstrate the feasibility of the approach.

Il est important que les logiciels pilotant les systèmes critiques (avions, centrales nucléaires, etc.) fonctionnent correctement — alors que la plupart des systèmes informatisés de la vie courante (micro-ordinateur, distributeur de billets, téléphone portable) ont des dysfonctionnements visibles. Il ne s'agit pas là d'un simple problème d'ingéniérie : on sait depuis les travaux de Turing et de Cook que la preuve de propriétés de bon fonctionnement sur les programmes est un problème intrinsèquement difficile.<br /><br />Pour résoudre ce problème , il faut des méthodes à la fois efficaces (coûts en temps et en mémoire modérés), sûres (qui trouvent tous les problèmes possibles) et précises (qui fournissent peu d'avertissements pour des problèmes inexistants). La recherche de ce compromis nécessite des recherches faisant appel à des domaines aussi divers que la logique formelle, l'analyse numérique ou l'algorithmique « classique ».<br /><br />De 2002 à 2007 j'ai participé au développement de l'outil d'analyse statique Astrée. Ceci m'a suggéré quelques développements annexes, à la fois théoriques et pratiques (utilisation de techniques de preuve formelle, analyse de filtres numériques...). Plus récemment, je me suis intéressé à l'analyse modulaire de propriétés numériques et aux applications en analyse de programme de techniques de résolution sous contrainte (programmation semidéfinie, techniques SAT et SAT modulo théorie).