Abstract Interpretation of Mobile Systems Jérôme Feret

138

pages

Français

Documents

Écrit par
Jérôme Feret

Publié par
pefav

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

138

pages

Français

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

pefav

Nombre de lectures

Langue

Français

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

Publié par

pefav

Nombre de lectures

Langue

Français

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

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 reconﬁgurables, •systèmes biologiques, •. . . .

Jérôme Feret

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: (conﬁnement,conﬁdentialité. . ), . 2.dénombrement des composants: (exclusions mutuelles,non-épuisement des ressources. . ), . 3. analyse desunités de calculs: (absence de conﬂit,authentiﬁcation,intégrité des mises à jour, . . . ).

Jérôme Feret

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

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 afﬁnes et intervalles). Publication : Feret — GETCO'00, JLAP'05

Jérôme Feret

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

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

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

January, 2009

Jérôme Feret

Dynamic linkage of agents

��