Abstract Interpretation of Mobile Systems Jérôme Feret

De
Publié par

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


Publié le : mardi 19 juin 2012
Lecture(s) : 14
Source : di.ens.fr
Nombre de pages : 138
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
A 1 1
Jérôme Feret
Dynamic creation of agents
A 2 1 2
11
A 3 2 3
...........
January, 2009
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.