Verification and mapping of unity programs into distributed architectures
Vérification et mise en œuvre distribuée des programmes unity
Abstract
Not available
L'affinement successif de programmes parallèles à partir de spécifications formelles permet de s'assurer de la correction du programme obtenu par rapport a la specification initiale, puisque la transformation est fondée sur la préservation de propriétés telles que celles d'invariance et celles de fatalité. Cependant, les programmes obtenus sont écrits dans une notation abstraite éloignée des langages de programmation parallèles classiques et il convient de développer des techniques de transformation de programmes (ensemble d'actions) en des programmes écrits dans des langages de programmation parallèles (linda, occam). Bien entendu, cela conduit à analyser les techniques possibles de parallélisation de systèmes d'actions ou de distribution de systèmes d'actions. Notre travail de thèse s'appuie sur le formalisme unity de Chandy et Misra pour lequel nous avons construit un outil d'aide à la preuve dans l'outil b et nous avons examiné plusieurs types de transformations de programmes unity en d'autres langages ainsi que des stratégies de répartition. Nous proposons un langage intermédiaire que nous dénommons UCL (unity communication language) qui facilite l'implantation d'unity sur une architecture parallèle, et qui assure la correction formelle de cette implantation vis-à-vis de la spécification initiale. Le langage UCL est ensuite utilisé comme nouveau point de départ de la transformation et permet de produire soit un programme Clinda, soit un programme Occam. Cette approche favorise la réutilisation de cette première étape de transformation avant de cibler une architecture particulière