Les systèmes embarqués complexes (avions, satellites, drones...) contiennent de plus en plus de calculateurs. Désormais ce sont des dizaines voire des centaines de calculateurs qui communiquent à travers un réseau partagé. Une fonction est réalisée par la collaboration d'un ensemble de calculateurs qui s'échangent un nombre croissant d'informations. Dans un contexte de temps réel embarqué, il faut non seulement garantir que ces informations échangées sont correctes mais il faut aussi garantir qu'elles vérifient leurs contraintes temporelles. Du point de vue du réseau cela signifie qu'une information doit être échangée en respectant les délais qui lui sont imposés. Ceci implique de pouvoir borner le temps de traversée du réseau de chaque message afin de vérifier qu'il arrive dans les temps. Or les systèmes embarqués étant de plus en plus complexes et le nombre d'informations échangées étant en constante augmentation, cette borne est de plus en plus difficile à calculer. De plus il est important que cette borne soit le moins pessimiste possible afin d'éviter que le système soit surdimensionné. L'objectif de ce travail est de mettre en place un modèle capable de calculer ces bornes.Afin d'y parvenir nous nous sommes basés sur la méthode d'analyse du Calcul Réseau.Ce travail s'est en particulier attardé sur la modélisation des interactions qui existent entre les messages synchrones et les messages asynchrones. Les modèles présentés dans ce manuscrit prennent en compte les dates d'émission sur le réseau des messages synchrones lors du calcul des bornes supérieures de temps de traversée des messages asynchrones.Les principales contributions apportées par ce manuscrit sont :1. la présentation d'une nouvelle façon d'envisager l'utilisation des dates d'émission sur le bus CAN : la synchronisation faible.Ainsi que la modélisation complète d'un tel système et enfin l'évaluation du gain apporté par cette solution.2. une modélisation complète du réseau TTEthernet permettant d'évaluer finement l'impact des flux synchrones sur le tempsde traversée des flux asynchrones.3. une présentation de l'utilisation de la synchronisation dans le réseau TSN ainsi qu'un modèlecomplet permettant d'analyser cette nouvelle technologie. / Complex embedded systems (planes, satellites, drones ...) contain more and more calculators. From now on, these are tens or even hundreds of calculators that communicate through a shared network. A function is achieved by the collaboration of a set of devices that exchange a growing number of information. In an embedded real-time context, it must be ensured that these informations exchanged are correct but it must also be ensured that they verify their temporal constraints. From the network point of view, this means that informations must be exchanged respecting their deadlines. This implies being able to upper bound the traversal time of the network of each message in order to verify that it arrives in time. However, as embedded systems are more and more complex and as the amount of information exchanged is constantly increasing, this bound is increasingly difficult to compute. Furthermore, it is important that this upper bound to be the least pessimistic possible to avoid an oversized system.The goal of this work is to develop new methods of analysis in order to be able to compute these bounds.In order to achieve this, we used the Network Calculus method of analysis.This work focuses on the modeling of interactions between synchronous messages and asynchronous messages.The models presented in this work take into account the transmission dates on the network of synchronous messageswhen calculating the upper bounds of traversal time of the asynchronous messages.The main contributions are:1. the presentation of a new way of considering the use of the dates of emission on the CAN bus: the weak synchronization.As well as the complete modeling of such a system and finally the evaluation of the gain provided by this solution.2. a complete modeling of the TTEthernet network allowing to evaluate the impact of the synchronous flows on the traversal time of the asynchronous flows.3. a presentation of the use of synchronization in the TSN network and a complete model for analyzing this new technology.

Dans le cadre d'une thèse CIFRE conjointe entre le Loria et Thales Research & Technology, nous étudions un nouveau type de réseau maillé embarqué temps réel. La mise en réseau maillé des composants des systèmes embarqués concilie les contraintes temps réel des applications avec leurs besoins croissants en termes de bande passante et collaboration. La pluralité des chemins de communication résulte en de meilleures propriétés de flexibilité, résilience, passage à l'échelle et répartition de charge. Cependant, ceci nécessite d'être capable d'allouer dynamiquement les ressources réseau en fonction des besoins des applications. Notre approche consiste à permettre aux applications de faire des requêtes de flux temps réel à l'exécution, puis allouer dynamiquement les ressources correspondant aux besoins en communication. A cette fin, nous avons conçu l'architecture Software-Defined Real-time Networking (SDRN). Elle aborde en même temps les problématiques d'isolation des flux, analyse temporelle, routage, tolérance aux fautes, ainsi que les interfaces avec les couches applicatives et les couches basses du système. Elle est également modulaire, c'est-à-dire que certaines parties de l'architecture peuvent être remplacées sans remettre en cause les autres modules. Enfin, elle a été validée par une implémentation sur plateforme matérielle RapidIO. Ce document restitue les travaux de recherche sur SDRN. Il s'intéresse également à la problématique de l'expérimentation sur les réseaux embarqués et propose une approche originale d'expérimentation, ERICA. Cette approche facilite la mise en place d'expérimentations mêlant aspects réels et simulés. ERICA génère les fichiers nécessaires à la mise en place du scénario défini dans une interface graphique haut niveau. Elle permet ainsi au chercheur d'appliquer une réflexion haut niveau sur ses expérimentations et de réutiliser les couches communes à plusieurs scénarios d'expérimentation / We are studying a new kind of embedded real-time mesh network. Mesh networking of the components of embedded systems reconciles their real-time constraints with the new application needs in terms of bandwidth and tight interactions. The plurality of communication paths results in increased flexibility, resilience, scalability and load balancing characteristics. However, this requires the ability to dynamically allocate network resource with respect to the needs of running applications. Our approach is to allow applications to make online real-time flow resource requests and consequently allot network resources according to these requirements. To this end, we have designed the Software-Defined Real-time Networking (SDRN) architecture. It addresses flow isolation, timing analysis, routing, fault tolerance, as well as the interfaces with the application layer and the lower layers of the system. It also allows any module to be replaced without interfering with the remainder of the architecture. It has been validated via an implementation on an in-silicon RapidIO platform. This thesis describes our research on the SDRN architecture. It also proposes an original method for experimenting on embedded networks, ERICA. The ERICA framework automatically generates all what is needed to conduct a network experiment in a selected environment (such as a simulator or a testbed), with both physical and simulated aspects. Hence, it allows the researcher to perform a high-level thinking of the whole experimentation process and to reuse applications and experiment designs from an experimentation stack to another

Cette thèse expose nos travaux de certification d'une partie d'un programme C/C++ nommé SimSoC (Simulation of System on Chip), qui simule le comportement d'architectures basées sur des processeurs tels que ARM, PowerPC, MIPS ou SH4. Un simulateur de System on Chip peut être utilisé pour developper le logiciel d'un système embarqué spécifique, afin de raccourcir les phases des développement et de test, en particulier quand la vitesse de simulation est réaliste (environ 100 millions d'instructions par seconde par cœur dans le cas de SimSoC). Les réductions de temps et de coût de développement obtenues se traduisent par des cycles de conception interactifs et rapides, en évitant la lourdeur d'un système de développement matériel. SimSoC est un logiciel complexe, comprenant environ 60 000 de C++, intégrant des parties écrites en SystemC et des optimisations non triviales pour atteindre une grande vitesse de simulation. La partie de SimSoC dédiée au processeur ARM, l'un des plus répandus dans le domaine des SoC, transcrit les informations contenus dans un manuel épais de plus de 1000 pages. Les erreurs sont inévitables à ce niveau de complexité, et certaines sont passées au travers des tests intensifs effectués sur la version précédente de SimSoC pour l'ARMv5, qui réussissait tout de même à simuler l'amorçage complet de linux. Un problème critique se pose alors : le simulateur simule-t-il effectivement le matériel réel ? Pour apporter des éléments de réponse positifs à cette question, notre travail vise à prouver la correction d'une partie significative de SimSoC, de sorte à augmenter la confiance de l'utilisateur en ce similateur notamment pour des systèmes critiques. Nous avons concentré nos efforts sur un composant particulièrement sensible de SimSoC : le simulateur du jeu d'instructions de l'ARMv6, faisant partie de la version actuelle de SimSoC. Les approches basées sur une sémantique axiomatique (logique de Hoare par ex- emple) sont les plus répandues en preuve de programmes impératifs. Cependant, nous avons préféré essayer une approche moins classique mais plus directe, basée sur la sémantique opérationnelle de C : cela était rendu possible en théorie depuis la formalisation en Coq d'une telle sémantique au sein du projet CompCert et mettait à notre disposition toute la puissance de Coq pour gérer la complexitité de la spécification. À notre connaissance, au delà de la certification d'un simulateur, il s'agit de la première expérience de preuve de correction de programmes C à cette échelle basée sur la sémantique opérationnelle. Nous définissons une représentation du jeu d'instruction ARM et de ses modes d'adressage formalisée en Coq, grâce à un générateur automatique prenant en entrée le pseudo-code des instructions issu du manuel de référence ARM. Nous générons également l'arbre syntaxique abstrait CompCert du code C simulant les mêmes instructions au sein de Simlight, une version allégée de SimSoC. À partir de ces deux représentations Coq, nous pouvons énoncer et démontrer la correction de Simlight, en nous appuyant sur la sémantique opérationnelle définie dans CompCert. Cette méthodologie a été appliquée à au moins une instruction de chaque catégorie du jeu d'instruction de l'ARM. Au passage, nous avons amélioré la technologie disponible en Coq pour effectuer des inversions, une forme de raisonnement utilisée intensivement dans ce type de situation. / Approaches based on axiomatic semantics (typically, Hoare logic) are the mostpopular for proving the correctness of imperative programs. However, we prefered totry a less usual but more direct approach, based on operational semantics : this wasmade possible in theory since the development of an operational semantics for theC language formalized in Coq in the CompCert project, and allowed us to use thecomfortable logic of Coq, of much help for managing the complexity of the specification.Up to our knowledge, this is the first development of formal correctness proofs basedon operational semantics, at least at this scale.We provide a formalized representation of the ARM instruction set and addressingmodes in Coq, using an automatic code generator from the instruction pseudo-code inthe ARM reference manual. We also generate a Coq representation of a correspondingsimulator in C, called Simlight, using the abstract syntax defined in CompCert.From these two Coq representations, we can then state and prove the correctnessof Simlight, using the operational semantics of C provided by CompCert. Currently,proofs are available for at least one instruction in each category of the ARM instructionset.During this work, we improved the technology available in Coq for performinginversions, a kind of proof steps which heavily occurs in our setting.

L'Internet des objets (IoT : Internet-of-Things) a été favorisé par les progrès accélérés dans les technologies de communication, les technologies de calcul, les technologies de capteurs, l'intelligence artificielle, l'informatique en nuage et les technologies des semi-conducteurs. En générale, l'IoT utilise l'informatique en nuage pour traitant les données, l'infrastructure de communication (y compris l’Internet) et des nœuds de capteurs pour collecter des données, de les envoyer de l'infrastructure du réseau à l’Internet, et de recevoir des commandes pour réagir à l'environnement. Au cours de ses opérations, l'IoT peut collecter, transmettre et traiter des données secrètes ou privées, ce qui pose des problèmes de sécurité. La mise en œuvre des mécanismes de sécurité pour l'IoT est un défi, car les organisations de l’IoT incluent des millions de périphériques intégrés à plusieurs couches, chaque couche ayant des capacités de calcul et des exigences de sécurité différentes. En outre, les nœuds de capteurs dans l'IoT sont conçus pour être des périphériques limités par une batterie, avec un budget de puissance, des calculs et une empreinte mémoires limités pour réduire les coûts d’implémentation. L'implémentation de mécanismes de sécurité sur ces appareils rencontre même plus de défis. Ce travail est donc motivé pour se concentrer sur l’implémentation du cryptage des données afin de protéger les nœuds et les systèmes de capteurs IoT en tenant compte du coût matériel, du débit et de la consommation d’énergie. Pour commencer, un crypto-accélérateur de chiffrement de bloc ultra-basse consommation avec des paramètres configurables est proposé et implémenté dans la technologie FDSOI ST 28 nm dans une puce de test, qui est appelée SNACk, avec deux modules de cryptographie : AES et PRESENT. L’AES est un algorithme de cryptage de données largement utilisé pour l’Internet et utilisé actuellement pour les nouvelles propositions IoT, tandis que le PRESENT est un algorithme plus léger offrant un niveau de sécurité réduit mais nécessitant une zone matérielle beaucoup plus réduite et une consommation très bas. Le module AES est une architecture de chemin de données 32 bits contenant plusieurs stratégies d'optimisation prenant en charge plusieurs niveaux de sécurité, allant des clés 128 bits aux clés 256 bits. Le module PRESENT contient une architecture à base arrondie de 64 bits pour optimiser son débit. Les résultats mesurés pendant cette thèse indiquent que ce crypto-accélérateur peut fournir un débit moyen (environ 20 Mbits/s au 10 MHz) tout en consommant moins de 20 µW dans des conditions normales et une sous-pJ d’énergie par bit. Cependant, la limitation du crypto-accélérateur réside dans le fait que les données doivent être lues dans le crypto-accélérateur et réécrites en mémoire, ce qui augmente la consommation d'énergie. Après cela, afin de fournir un haut niveau de sécurité avec une flexibilité et une possibilité de configuration pour s’adapter aux nouvelles normes et pour atténuer les nouvelles attaques, ces travaux portent sur une approche novatrice de mise en œuvre de l’algorithme de cryptographie utilisant la nouvelle SRAM proposée en mémoire. Le calcul en mémoire SRAM peut fournir des solutions reconfigurables pour mettre en œuvre diverses primitives de sécurité en programmant les opérations de la mémoire. Le schéma proposé consiste à effectuer le chiffrement dans la mémoire en utilisant la technologie Calcul en Mémoire (In-Memory-Computing). Ce travail illustre deux mappages possibles de l'AES et du PRESENT à l'aide du calcul en mémoire. / The Internet of Things (IoT) has been fostered by accelerated advancements in communication technologies, computation technologies,sensor technologies, artificial intelligence, cloud computing, and semiconductor technologies. In general, IoT contains cloud computing to do data processing, communication infrastructure including the Internet, and sensor nodes which can collect data, send them through the network infrastructure to the Internet, and receive controls to react to the environment. During its operations, IoT may collect, transmit and process secret data, which raise security problems. Implementing security mechanisms for IoT is challenging because IoT organizations include millions of devices integrated at multiple layers, whereas each layer has different computation capabilities and security requirements. Furthermore, sensor nodes in IoT are intended to be battery-based constrained devices with limited power budget, limited computation, and limited memory footprint to reduce costs. Implementing security mechanisms on these devices even encounters more challenges. This work is therefore motivated to focus on implementing data encryption to protect IoT sensor nodes and systems with the consideration of hardware cost, throughput and power/energy consumption. To begin with, a ultra-low-power block cipher crypto-accelerator with configurable parameters is proposed and implemented in ST 28nm FDSOI technology in SNACk test chip with two cryptography modules: AES and PRESENT. AES is a widely used data encryption algorithm for the Internet and currently used for new IoT proposals, while PRESENT is a lightweight algorithm which comes up with reduced security level but requires with much smaller hardware area and lower consumption. The AES module is a 32-bit datapath architecture containing multiple optimization strategies supporting multiple security levels from 128-bit keys up to 256-bit keys. The PRESENT module contains a 64-bit round-based architecture to maximize its throughput. The measured results indicate that this crypto-accelerator can provide medium throughput (around 20Mbps at 10MHz) while consumes less than 20uW at normal condition and sub-pJ of energy per bit. However, the limitation of crypto-accelerator is that the data has to be read into the crypto-accelerator and write back to memory which increases the power consumption. After that, to provide a high level of security with flexibility and configurability to adapt to new standards and to mitigate to new attacks, this work looks into an innovative approach to implement the cryptography algorithm which uses the new proposed In-Memory-Computing SRAM. In-Memory Computing SRAM can provide reconfigurable solutions to implement various security primitives by programming the memory's operations. The proposed scheme is to carry out the encryption in the memory using the In-Memory-Computing technology. This work demonstrates two possible mapping of AES and PRESENT using In-Memory Computing.

Depuis quelques années, avec les progrès en électronique de puissance et pour améliorer les performances, le confort et la sécurité des utilisateurs, l'électricité devient le vecteur énergétique principal en remplacement de l'hydraulique et du pneumatique dans les domaines de l'automobile, du naval et de l'aéronautique.<br /> Airbus ne se situe pas en dehors de cette évolution. Son objectif à moyen terme est de rationaliser l'énergie à bord pour aller vers un avion de plus en plus électrique : les systèmes alimentés par l'énergie hydraulique et pneumatique (commande de vol, conditionnement d'air...) seront remplacés par l'énergie électrique, plus facile à acheminer. Ainsi, la puissance électrique installée augmente rapidement : 275 kVA pour l'Airbus A320, 900 kVA pour l'Airbus 380, autour de 1 MVA pour le futur Airbus A30X de type «bleedless ». Pour répondre aux enjeux posés par cette montée en puissance, une nouvelle architecture du système électrique est nécessaire. <br /> L'objectif de cette thèse est d'étudier et de créer des méthodes et des outils pour l'optimisation du dimensionnement d'un système électrique embarqué de manière à répondre à un certain nombre de critères (masse, coût, fiabilité) tout en respectant un certain nombre de contraintes (qualité réseau, stabilité). Ces méthodes et outils sont ici utilisés pour traiter le problème de la conception : un canal de puissance d'un réseau du bord de la nouvelle génération d'avion Airbus (type «bleddless »).

Notre proposition consiste à présenter un modèle et une infrastructure d'exécution orienté composant pour le domaine des applications multi-tâches à contraintes temps réel souples et embarquées (nommé Tinap).<br /><br />Nous définissons un modèle de composant reposant sur plusieurs vues : une vue structurelle, placée au centre du cycle de conception, reposant initialement sur le modèle Fractal, une vue dynamique permettant au concepteur, dans une démarche descriptive, de personnaliser l'architecture métier pour définir les aspects de son applicatif liés à la concurrence, et enfin une vue implantation et une vue comportement fournissant respectivement une abstraction de l'implantation interne des composants et de leur comportement à l'égard de leur environnement. De plus, notre proposition est intégrée à un cadre méthodologique dirigé par les modèles.<br /><br />Nous avons également expérimenté le paradigme composant à différents niveaux d'abstraction : pour l'applicatif et pour celui de l'infrastructure d'exécution qui les implante. Enfin, au niveau du système d'exploitation fournissant les services élémentaires nécessaires. Cette démarche est motivée par la volonté d'exploiter notre modèle multi-vues canonique et de l'adapter en fonction des besoins de chaque niveau d'abstraction. Cette expérimentation est menée avec Think, une implantation en C des spécifications Fractal.<br /><br />Nous expérimentons Tinap par deux cas d'étude que nous avons prototypés. En premier lieu, pour concevoir une application d'analyse et de contrôle de flux multimédias par l'intermédiaire de disques vinyles. En second lieu pour expérimenter la mise en oeuvre du modèle d'exécution Accord (une méthodologie de conception pour applications temps-réel).

Cette thèse d'Habilitation à Diriger des Recherches revient sur une dizaine d'années de contributions théoriques et pratiques à l'optimisation combinatoire, contributions dont le domaine d'application privilégié est l'optimisation des systèmes de télécommunications (principalement les autocommutateurs pour la téléphonie cellulaire) et informatiques (en particulier les architectures de processeur parallèles, dites multi-cœurs). Ces travaux se caractérisent également par la résolution bout-en-bout de nombreux cas d'applications industriels concrets et difficiles, de la modélisation mathématique initiale jusqu'à la mise en œuvre d'algorithmes de résolution opérationnels en passant par les développements théoriques nécessaires à leurs fondements.

Concernant la partie logicielle des systèmes embarqués, on constate le besoin d'un modèle de la structuration du logiciel qui facilite le processus de développement, la capacité de faire évoluer le comportement du système lors de son exécution, afin de s'adapter aux changements de son environnement, et la prise en compte des limitations des ressources physiques des plates-formes d'exécution. L'utilisation de composants logiciels est une approche de conception qui, via l'abstraction des détails techniques, facilite la gestion de la complexité du logiciel. La question que nous nous posons est: comment les composants doivent être développés de façon à satisfaire les exigences liées aux fortes contraintes physiques et au besoin d'évolution du logiciel ? Pour y répondre, nous introduisons a notion de réification de composant. Une réification est une collection de données et de comportements qui encapsulent des aspects du composant à un moment précis de son cycle de vie. Nous proposons ensuite des techniques d'optimisation pour la génération du code "glue" qui assure l'interopérabilité des composants, afin de satisfaire les contraintes liées aux ressources limitées. Elles rendent possible la définition de niveaux d'optimisation pour chaque instance des entités du modèle à composants, ce qui nous permet de régler la performance du logiciel en fonction de ses besoins (extra) fonctionnels. Ensuite, nous définissons quatre profils d'évolution en fonction des caractéristiques d'évolution de chaque entité du modèle, et nous mettons en place des infrastructures d'évolution adaptées aux besoins d'évolution du système, couplées avec les exigences de performance du logiciel.

Dans cette étude, nous nous intéressons aux outils de génération de logiciel embarqué ciblant des plateformes multi-tuiles hétérogènes. Dans ces plateformes, un système sur puce multiprocesseurs hétérogène (ou tuile) est répliqué et connecté par des réseaux externes à la tuile, extensibles et commutés par paquets. Ces outils se basent sur une représentation abstraite de l'architecture, de l'application et du déploiement des éléments applicatifs sur les éléments de l'architecture. Programmer de zéro ces architectures complexes n'est pas concevable, cependant nous ne pouvons nous contenter des environnements de programmation embarqués classiques en raison de l'hétérogénéité de la tuile de base, qui embarque des RISCs, des DSPs et une infrastructure interne à la tuile non uniforme et complexe. L'un des enjeux dans ce contexte est de masquer cette complexité au programmeur de l'application pour qu'il puisse se concentrer sur l'écriture de son programme sans se soucier dans un premier temps de son déploiement sur la plateforme cible. L'une des difficultés des systèmes multi-tuiles est le nombre de chemins de communication que ceux-ci proposent, c'est pourquoi nous nous concentrons dans ce manuscrit sur la gestion (transparente pour le programmeur) des communications dans notre flot. Nous définissons donc les informations minimales à inclure dans le modèle d'entrée du flot pour arriver à synthétiser les communications de l'application. Grâce à ces informations, nous arrivons à puiser les composants logiciels de communication adéquats, qui se présentent sous la forme de pilotes d'un système d'exploitation. Cette sélection n'est pas suffisante, il faut ensuite spécialiser ces composants pour chaque canal de communication de l'application afin d'arriver à un résultat correct. En raison du nombre d'unités de calcul de la plateforme ciblée et du nombre de canaux des applications considérées, une automatisation totale du flot est requise, nous abordons donc les difficultés que cela représente en raison du processus de compilation croisé mis en jeu par le flot, et la solution que nous avons retenue pour arriver à un flot fonctionnel. Trois applications (dont une appartenant au monde du calcul de haute performance), écrites par des programmeurs ne maîtrisant pas la plateforme multi-tuiles choisie, ont été soumises à notre flot, qui a généré de manière correcte plusieurs déploiements de ces applications.

Cette thèse a été co-encadrée par le laboratoire MAPS/AMS de France Telecom R&D (aujourd'hui MAPS/SHINE) et le laboratoire VERIMAG. Le développement de logiciels pour les systèmes embarqués présente de nombreux défis. Cette thèse s'intéresse à ceux posés par les interactions entre les trois phases de conception (les développeurs construisent à partir de spécifications un modèle du système exprimé dans un langage de conception i.e. de programmation), d'implantation (le modèle précédent est compilé en un exécutable du système qui est finalement déployé sur les plateformes réelles) et de validation (un ensemble de techniques sont mises en \oe uvre pour vérifier que le système implanté est correct vis-à-vis des spécifications). Pour cela nous nous intéressons aux caractéristiques du langage de conception et aux techniques de compilation de ce langage. Celles-ci permettent d'obtenir dans notre approche à la fois l'implantation du système et un modèle du système implanté. L'analyse de ce modèle permet la validation de l'implantation, ce qui suppose que ce modèle représente fidèlement le système implanté. Nous proposons la construction d'un langage de conception basé sur l'utilisation de composants logiciels prédéfinis dont le comportement dynamique est supposé connu. Nous illustrons cette démarche par la réalisation d'un prototype complet d'un langage appelé Buzz, inspiré des modèles de programmation à acteurs dans lequel les composants logiciels utilisés sont des composants Think accompagnés de leur modèle comportemental opérationnel constitué d'un composant BIP. Le compilateur associé à Buzz que nous avons développé à partir du compilateur Think existant (Nuptse) génère simultanément une architecture à composants Think pour l'implantation et un modèle à composants BIP à des fins d'analyse. Nous évaluons Buzz à travers deux expériences. La première présente le développement de bout en bout d'un logiciel pour un exemple académique sur lequel nous démontrons la pertinence des choix techniques. Think nous permet un support d'implantation complet (compilation, optimisation, déploiement) et BIP rend possible la vérification d'un ensemble de propriétés dynamiques du système. La deuxième expérience consiste à porter une application réelle de protocole radio utilisée dans des réseaux de capteurs et développée de manière classique, vers Buzz. Cette expérience démontre l'effectivité de notre proposition tant en termes de langage de programmation (l'expressivité de Buzz structure et simplifie le code original) qu'en termes d'outils de compilation et de vérification.