Modèles de programmation de haut niveau pour microcontrôleurs à faibles ressources

Microcontrollers are programmable integrated circuit embedded in multiple everyday objects. Due to their scarce resources, they often are programmated using low-level languages such as C or assembly languages. These languages don't provide the same abstractions and guarantees than higher-level programming languages, such as OCaml. This thesis offers a set of solutions aimed at extending microcontrollers programming with high-level programming paradigms. These solutions provide multiple abstraction layers which, in particular, enable the development of portable programs, free from the specifics of the hardware. We thus introduce a layer of hardware abstraction through an OCaml virtual machine, that enjoys the multiple benefits of the language, while keeping a low memory footprint. We then extend the OCaml language with a synchronous programming model inspired from the Lustre dataflow language, which offers abstraction over the concurrent aspects of a program. The language is then formally specified and various typing properties are proven. Moreover, the abstractions offered by our work induce portability of some static analyses that can be done over the bytecode of programs. We thus propose such an analysis that consists of estimating the worst case execution time (WCET) of a synchronous program. All the propositions of this thesis form a complete development toolchain, and several practical examples that illustrate the benefits of the given solutions are thus provided.Les microcontrôleurs sont des circuits imprimés programmables nichés dans de nombreux objets de notre quotidien. En raison de leurs ressources limitées, ils sont souvent programmés dans des langages de bas niveau comme le C, ou en langage assembleur. Ces derniers n'offrent pas les mêmes abstractions et les mêmes garanties que des langages de haut niveau, comme OCaml. Cette thèse propose alors un ensemble de solutions destinées à enrichir la programmation de microcontrôleurs avec des paradigmes de programmation de plus haut niveau. Ces solutions apportent une montée en abstraction progressive, permettant notamment de réaliser des programmes indépendants du matériel utilisé. No présentons ainsi une première abstraction du matériel prenant la forme d’une machine virtuelle OCaml, qui permet de profiter des nombreux avantages du langage tout conservant une faible empreinte mémoire. Nous étendons par la suite OCaml avec un modèle de programmation synchrone inspiré du langage Lustre et permettant d'abstraire les aspects concurrents d’un programme. Une spécification formelle du langage est donnée, et plusieurs propriétés de typage sont par la suite vérifiées. Les abstractions offertes par nos travaux induisent par ailleurs la portabilité de certaines analyses statiques pouvant être réalisées sur le bytecode des programmes. Une telle analyse, servant à estimer le temps d’exécution pire-cas d’un programme synchrone, est alors proposée. L'ensemble des propositions de cette thèse constitue une chaîne complète de développement, et plusieurs exemples d’applications concrètes illustrant la complétude des solutions offertes sont alors présentées