Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Abstract Interpretation of Mobile Systems Jérôme Feret

De
138 pages
MPRI Abstract Interpretation of Mobile Systems Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure INRIA, ÉNS, CNRS feret January, 2009

  • approche indépendante du modèle

  • laboratoire d'informatique de l'ecole normale

  • composants récursifs

  • analyse des liaisons dynamiques entre les composants

  • système biologique


Voir plus Voir moins
MPRI
Abstract Interpretation of Mobile Systems
Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure INRIA, ÉNS, CNRS rf/d..ine.sthwww//:ptefert
January, 2009
1. 2. 3. 4. 5. 6. 7. 8.
Overview
Overview Mobile systems Non standards semantics Abstract Interpretation Environment analyses Occurrence counting analysis Thread partitioning Conclusion
Jérôme Feret
2
January, 2009
Systèmes mobiles
Un ensemble de composants qui interagissent. Ces interactions permettent de : synchroniser l'exécution de ces composants, changer les liaisons entre les composants, créer des nouveaux composants. Le nombre de composants n'est pas borné ! Champs d'application : protocoles de communication, protocoles cryptographiques, systèmes reconfigurables, systèmes biologiques, . . . .
Jérôme Feret
3
January, 2009
Démarche Construction de sémantiques abstraites : correctes,automatiques,décidables, maisapprochées(indécidabilité).
Approche indépendante du modèle: 1. conception d'unMETA-langage pour encoder les modèles existants ; 2. développement d'analyses au niveau de ceMETA-langage.
Trois familles d'analyses: 1. analyse desliaisons dynamiques entre les composants: (confinement,confidentialité. . ), . 2.dénombrement des composants: (exclusions mutuelles,non-épuisement des ressources. . ), . 3. analyse desunités de calculs: (absence de conflit,authentification,intégrité des mises à jour, . . . ).
Jérôme Feret
4
January, 2009
Analyse des liaisons entre les composants : Quels composants peuvent interagir ?
client creation
clients
server instances
L'analyse distingue les composants récursifs Domaines abstraits:relations entre des mots. Publications : Feret — SAS'00, SAS'01, ESOP'02, JLAP'05
Jérôme Feret
5
server
January, 2009
Analyse du nombre des composants : Borne le nombre de composants
création des clients
clients
instances du serveur
serveur deux ports
client rouge en attente...
Nouveau domaine abstrait:relations numériques (invariants affines et intervalles). Publication : Feret — GETCO'00, JLAP'05
Jérôme Feret
6
January, 2009
Partitionnement de tâches
Principe : regrouper les composants en unités de calcul, =grâce à l'analyse des liaisons entre les composants ; compter le nombre de composants dans chaque unité de calcul, =grâce à l'analyse de dénombrement. Intérêt: chaque session est isolée,
ce qui permetaux analyses de se focaliser sur chacune des sessions.
Jérôme Feret
7
January, 2009
1. 2. 3. 4. 5. 6. 7. 8.
Overview
Overview Mobile systems Non standards semantics Abstract Interpretation Environment analyses Occurrence counting analysis Thread partitioning Conclusion
Jérôme Feret
8
January, 2009
Mobile system
A pool of processes which interact and communicate:
Interactions control:
process synchronization; update of link between processes (communication, migration); process creation.
The number of processes may be unbounded !
Jérôme Feret
9
January, 2009
Jérôme Feret
Dynamic linkage of agents
A

C
10

B

January, 2009
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin