La modélisation et la spécification de systèmes distribués nécessitent une adaptation des modèles logiques utilisés pour leur représentation. Les notions<br />d'emplacements et de ressources jouent notamment un rôle centrale dans la représentation de ces systèmes.<br /><br />On propose tout d'abord à la proposition d'une première logique, la logique linéaire distribuée et mobile (DMLL) qui intègre les notions de distribution et de mobilité. On propose également une sémantique à la Kripke et un calcul des séquents supportant l'élimination des coupures pour cette logique.<br /><br />Cette première étude a mis en avant le rôle centrale de la sémantique pour la modélisation de systèmes distribués. On propose alors la structure des arbres de ressources, des arbres dont les noeuds possèdent des labels et contiennent des ressources appartenant à<br />monoïde partiel de ressources et BI-Loc, une logique pour raisonner sur ces arbres, un langage permettant de modifier les arbres et son axiomatisation correcte et complète sous forme de triplets de Hoare. Concernant BI-Loc, on détermine des conditions suffisantes pour décider de la satisfaction et de la validité par model-checking et on développe une méthode de preuves fondée sur les tableaux sémantiques correcte et complète.<br /><br />On montre comment on peut raisonner sur les tas de pointeurs grâce aux arbres de ressources. Enfin, on détermine comment le modèle des arbres partiel peut être utilisé pour représenter et spécifier les données<br />semi-structurées et raisonner sur la transformation de ce type de données.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00128631 |
| Date | 09 December 2005 |
| Creators | Biri, Nicolas |
| Publisher | Université Henri Poincaré - Nancy I |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0019 seconds