Répartition modulaire de programmes synchrones
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 con...
| Main Author: | |
|---|---|
| Language: | FRE |
| Published: |
2008
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-00750832 http://tel.archives-ouvertes.fr/docs/00/75/08/32/PDF/these-delaval.pdf |
| Summary: | 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. |
|---|