Ce travail de thèse s'intègre dans le cadre du développement de nouvelles approches de conception afin de réduire significativement la consommation électrique des Systèmes sur Puce (SoC)ou des Objets Communicants utilisés pour traiter numériquement des signaux. Le but est alors d'obtenir des systèmes entièrement contrôlés par les événements contenus dans les signaux. Dans ce contexte, une nouvelle catégorie de chaîne de traitement est définie, associant une implémentation matérielle asynchrone (sans horloge globale) et un échantillonnage non uniforme dans le temps dit « par traversée de niveaux ». Un convertisseur Analogique/Numérique dédié à<br />cette tâche ayant déjà été réalisé, ce travail se focalise sur le traitement des données composées de couples amplitude-temps dont cette thèse montre que toute opération doit obligatoirement prendre en compte l'information temporelle. Des filtres numériques à réponse impulsionnelle finie (RIF) et infinie (RII) sont alors définis dans le cadre de signaux échantillonnés non uniformément. Des architectures sont proposées puis comparées à celles utilisées classiquement montrant que la complexité combinatoire était accrue. Un critère sur le choix de la technologie à privilégier, spécifiant la charge de calcul totale sur une durée finie, montre alors qu'en diminuant le nombre de points traités, l'approche asynchrone peut compenser le surcoût de complexité. Ainsi le traitement de signaux faiblement actifs par une chaîne asynchrone, combinant échantillonnage non uniforme et conception asynchrone, permet de réduire son activité moyenne et donc la consommation du circuit intégré, rendant cette technologie très attractive pour le domaine des SoC.

Ce travail de thèse s'intègre dans le cadre du développement de nouvelles approches de conception afin de réduire de manière significative la consommation électrique des Systèmes sur Puces (SoCs) ou des Objets Communicants. Le but est d'obtenir des systèmes uniquement contrôlés par les événements contenus dans le signal utile. Dans ce contexte, ce travail est focalisé sur un bloc critique dans de telles chaînes de traitement du signal : le Convertisseur Analogique Numérique (CAN). Il est donc décrit une nouvelle famille de CANs, mettant en œuvre un échantillonnage irrégulier dans le temps du signal analogique (échantillonnage par traversées de niveaux) et une implémentation asynchrone (pas d'horloge globale). Cette approche rend les caractéristiques de ces CANs duales par rapport à celles des CANs de Nyquist classiques : il y a échantillonnage en amplitude et quantification en temps. La théorie associée a conduit à développer une méthodologie de conception propre à ces convertisseurs. Connaissant les caractéristiques spectrales et statistiques du signal analogique, elle permet de déterminer les paramètres de conception optimaux du CAN afin de réduire le matériel mis en œuvre, son activité, et donc sa consommation électrique. Cette méthode a été utilisée pour la conception de CANs, en technologie CMOS standard 0,18µm. Les simulations électriques ont prouvé que leur Facteur de Mérite (FoM) atteint un ordre de grandeur de plus par rapport à celui des CANs de Nyquist actuels. L'étude de systèmes complets intégrant capteur, conversion analogique numérique et traitement numérique selon cette même méthode, utilisant simultanément de l'«asynchronisme» pour l'échantillonnage et l'implémentation matérielle, permet d'affirmer que des perspectives très intéressantes peuvent être espérées quant à la réduction de la dissipation d'énergie dans les SoCs.

L'utilisation des méthodes formelles pour la conception de protocoles de télécommunication est désormais reconnue comme la seule approche en mesure de garantir leur bon fonctionnement avant la mise en service. Cependant, la complexité toujours croissante ainsi que les contraintes de fiabilité et de sûreté de plus en plus sévères nécessitent l'extension des formalismes de description et l'amélioration continue des méthodes et des techniques de validation. Cette thèse définit une représentation intermédiaire nommé IF pour la description de protocoles. IF est construit à base d'automates temporisés communicants à échéances. Les échéances permettent la modélisation explicite de l'urgence des actions et sont un moyen très fin pour décrire l'évolution temporelle d'un système. Les automates communiquent soit de manière asynchrone, par files d'attente, soit de manière synchrone par rendez-vous. La sémantique opérationnelle de IF est formellement définie et des techniques de simulation efficaces sont proposées. De plus, ayant une structure statique, IF permet l'application intensive des techniques d'analyse statique, comme par exemple celles issues du domaine de l'optimisation de code. Certains informations calculées de cette manière peuvent améliorer considérablement les performances de la validation automatique. Une plate-forme ouverte de validation a été mise en place autour de IF. Elle intègre un grand nombre d'outils autant académiques que industriels et couvre la plupart des techniques actuellement employées pour la vérification et le test des protocoles. Cette plate-forme a été utilisée avec beaucoup de succès sur des protocoles de communication réels, comme par exemple SSCOP ou STARI.

Ce travail se situe dans le cadre de la vérification et de la validation des systèmes répartis, particulièrement les protocoles de télécommunication. Nous nous sommes intéressés au problème de la génération automatique de tests de conformité pour les protocoles de télécommunication et plus précisément à l'utilisation, en amont de TGV (un outil de génération de séquences de test), de techniques d'analyse statique. La génération de test de conformité fondée sur des techniques de vérification par modèles (l'approche employée par TGV) est limitée par le problème d'explosion d'état. Même si ce problème, dans la pratique, peut être contourné (en choisissant le fonctionnement à la volée de TGV), quelque aspects de cette méthode (par exemple la conception des objectifs de test pour un modèle, sans le construire explicitement) posent encore des problèmes. Dans notre thèse on propose une méthodologie de test basée sur des techniques issues des domaines de la vérification et de l'analyse statique. Cette méthodologie consiste en un ensemble de procédures qui ont pour but de simplifier la spécification en tenant compte de sa structure ou de la structure des objectifs de test et cela avant de la génération des cas de test. On réduit ainsi la taille des modèles observables des spécifications. Nous avons étendu aussi le concept de l'objectif de test. Les objectifs de test abstraits ont des contraintes symboliques attachées aux paramètres des signaux d'entrée. À partir des contraintes d'entrée les procédures mentionnées ci-dessus calculent des contraintes pour les paramètres des signaux de sortie des objectifs de test abstraits. Ensuite, des objectifs de test concrets pourront être dérivés et en utilisant l'outil de test existant TGV on pourrait générer des tests de conformité

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL.

Cette thèse se situe à l'intersection de deux domaines-clés : l'ingénierie dirigée par les modèles (IDM) et les méthodes formelles, avec différents champs d'application. Elle porte sur la vérification formelle d'applications parallèles modélisées selon l'approche IDM. Dans cette approche, les modèles tiennent un rôle central et permettent de développer une application par transformations successives (automatisées ou non) entre modèles intermédiaires à différents niveaux d'abstraction, jusqu'à la production de code exécutable. Lorsque les modèles ont une sémantique formelle, il est possible d'effectuer une vérification automatisée ou semi-automatisée de l'application. Ces principes sont mis en oeuvre dans TOPCASED, un environnement de développement d'applications critiques embarquées basé sur ECLIPSE, qui permet la vérification formelle par connexion à des boîtes à outils existantes. Cette thèse met en oeuvre l'approche TOPCASED en s'appuyant sur la boîte à outils CADP pour la vérification et sur son plus récent formalisme d'entrée : LOTOS NT. Elle aborde la vérification formelle d'applications IDM à travers deux problèmes concrets : 1) Pour les systèmes GALS (Globalement Asynchrone Localement Synchrone), une méthode de vérification générique par transformation en LOTOS NT est proposée, puis illustrée sur une étude de cas industrielle fournie par AIRBUS : un protocole pour les communications entre un avion et le sol décrit dans le langage synchrone SAM conçu par AIRBUS. 2) Pour les services Web décrits à l'aide de la norme BPEL (Business Process Execution Language), une méthode de vérification est proposée, qui est basée sur une transformation en LOTOS NT des modèles BPEL, en prenant en compte les sous-langages XML Schema, XPath et WSDL sur lesquels repose la norme BPEL. / The work in this thesis is at the intersection of two major research domains~: Model-Driven Engineering (MDE) and formal methods, and has various fields of application. This thesis deals with the formal verification of parallel applications modelled by the MDE approach. In this approach, models play a central role and enable to develop an application through successive transformations (automated or not) between intermediate models of differing levels of abstraction, until executable code is produced. When models have a formal semantics, the application can be verified, either automatically or semi-automatically. These principles are used in TOPCASED, an ECLIPSE-based development environment for critical embedded applications, which enables formal verification by interconnecting existing tools. This thesis implements the TOPCASED approach by relying on the CADP toolbox for verifying systems, and on its most recent input formalism : LOTOS NT. This thesis tackles the formal verification of MDE applications through two real problems : 1) For GALS (Globally Asynchronous, Locally Synchronous), a generic verification method, based on a transformation to LOTOS NT, is proposed and illustrated by an industrial case-study provided by AIRBUS : a communication protocol between the airplane and the ground described in the synchronous langage SAM designed at AIRBUS. 2) For Web services specified with the BPEL (Business Process Execution Language) norm, a verification method is proposed. It is based on a BPEL to LOTOS NT transformation which takes into account XML Schema, Xpath, and WSDL, the languages on which the BPEL norm is built.