Répartition modulaire de programmes synchrones

We address the problem of safe design of distributed embedded systems. We show that with the increasing complexity and integration of embedded systems, the functional structure of the system can conflict with the structure of its architecture. The usual approach of design by refinement of this architecture can then jeopardize the functional modularity of the system. We propose a method allowing the design of a distributed system as a unique program, which functional structure is independent of the system's architecture. This method is based on the extension of a synchronous dataflow programming language with primitives for program distribution. These primitives allow on one hand to describe the architecture as a graph defining existing computing resources and communication links between them, and on the other hand to specify by mean of annotations the localization of some values and computations of the program. We define the formal semantics of this extended language. The purpose of this semantics is to provide to the programmer a formal meaning to the annotations added to his program. A type and effect system is provided to ensure, at compilation time, the consistency of these annotations. A type inference mechanism allow the inference, from the annotations of the programmer, of the non-annotated values and computations. We finally define, from this type system, an automatic distribution method, allowing the computation, from an annotated program, of one program fragment for each computing resource of the architecture. The soundness of the type system with respect to the semantics has been proven, as well as the semantical equivalence of the composition of the fragments obtained via the automatic distribution method with the initial program. This method has been implemented in the compiler of the Lucid Synchrone language, and experimented with an example of software-defined radio.Nous nous intéressons à la conception sûre de systèmes répartis. Nous montrons qu'avec la complexité et l'intégration croissante des systèmes embarqués, la structure fonctionnelle du système peut entrer en conflit avec la structure de son architecture. L'approche traditionnelle de conception par raffinement de cette architecture compromet alors la modularité fonctionnelle du système. Nous proposons donc une méthode permettant de concevoir un système réparti défini comme un programme unique, dont la structure fonctionnelle est indépendante de l'architecture du système. Cette méthode est basée sur l'ajout de primitives de répartition à un langage flots de données synchrone. Ces primitives permettent d'une part de déclarer l'architecture sous la forme d'un graphe définissant les ressources existantes et les liens de communication existant entre ces ressources, et d'autre part de spécifier par des annotations la localisation de certaines valeurs et calculs du programme. Nous définissons ensuite la sémantique formelle de ce langage étendu. Cette sémantique a pour but de rendre compte de manière formelle l'effet des annotations ajoutées par le programmeur. Un système de types à effets permet ensuite de vérifier la cohérence de ces annotations. Ce système de types est muni d'un mécanisme d'inférence, qui permet d'inférer, à partir des annotations du programmeur, la localisation des calculs non annotés. Nous définissons ensuite, à partir de ce système de types, une méthode de répartition automatique permettant d'obtenir, à partir d'un programme annoté, un fragment de programme par ressource de l'architecture. La correction du système de types avec la sémantique du langage est prouvée, ainsi que l'équivalence sémantique de l'exécution des fragments obtenus par la méthode de répartition automatique avec le programme initial. Cette méthode a été implémentée dans le compilateur du langage Lucid Synchrone, et testée sur un exemple de radio logicielle