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.