Le développement de plus en plus important de services mobiles et d'applications distribuées et la volonté de développer des applications sûres nécessite une adaptation des outils de spécifications et de preuves pour mieux prendre en compte la distribution et la mobilité des ressources dans les systèmes informatiques. Dans cette optique, cette thèse propose tout d'abord une logique nommée logique linéaire distribuée et mobile (DMLL), fondée sur la logique linéaire et intégrant les notions d'emplacements et de déplacements. On propose un calcul des séquents pour cette logique où les preuves intégrent le déplacement des formules. On démontre l'élimination des coupures et on propose une sémantique à la Kripke correcte et complète pour cette logique. Enfin, on montre à travers une application pour la validation des protocoles d'authentification comment les modalités d'emplacement et de déplacement peuvent aider à l'analyse des attaques de protocoles. Pour cela, on représente les acteurs d'un protocole et leurs connaissances sous forme de formules logiques et on montre comment extraire des informations d'une preuve correspondant à une attaque. Cependant, DMLL est une logique définie pour être utilisée selon le paradigme proof-search-as-computation, selon lequel les formules correspondent à des progammes et les preuves correspondent à leur exécution. Ce choix est mal adapté pour modéliser et spécifier les propriétés de systèmes distribués. On propose donc un nouveau modèle logique fondé sur une structure adaptée à la représentation de systèmes distribués. Cette structure, l'arbre de ressources, consiste en un arbre dont les noeuds, qui sont étiquetés par des labels, contiennent des ressources appartenant à un monoïde d'arbres partiels. On présente ensuite une nouvelle logique, BI-Loc permettant de raisonner sur cette structure. Cette logique est fondée sur la logique BI et intègre une modalité d'emplacement permettant de raisonner sur la structure spatiale de arbres. On propose un langage de manipulation des arbres et une axiomatisation logique de ce langage sous forme de triplets de Hoare. On montre que la satisfaction et la décidabilité du model-checking pour la version propositionnelle de cette logique sont décidables. Pour la version avec quantificateurs, on démontre que le model-checking est indécidable et on determine des fragments décidables. On propose également une méthode de recherche de preuves avec tableaux sémantiques pour la version propositionnelle. On montre ensuite comment ce modèle peut être utilisé à travers plusieurs types d'applications. Concernant les modèles des pointeurs et des permissions, on montre que l'on peut utiliser une logique adaptée de BI-Loc pour exprimer des propriétés de ce modèle. Cette possibilité permet notamment d'exprimer sous forme d'une formule logique le typage des arbres dans le modèles des permissions, problème qui était sans solution avec des logiques de séparation classique. On détaille ensuite comment les arbres de ressources permettent de représenter la manipulation de documents XML et de raisonnner sur leur transformation. On présente en détails comment certaines règles de spécifications des documents XML se traduisent dans BI-Loc et on montre comment le modèle peut être utilisé pour valider les propriétés de certains programmes de transformation.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004526 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 004526 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Crin
   |étape=   Corpus
   |type=    RBID
   |clé=     CRIN:biri05
   |texte=   Logiques spatiales de ressources, modèles d'arbres et applications
}}