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
Università di Bologna Abstract interpretation of mobile systems Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure INRIA, ÉNS, CNRS feret Wednesday, April the 20th

  • laboratoire d'informatique de l'ecole normale

  • abstract interpretation

  • process creation

  • mobile system

  • links between


Voir plus Voir moins
Università di Bologna
Abstract interpretation of mobile systems
Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure INRIA, ÉNS, CNRS http://www.di.ens.fr/feret
Wednesday, April the 20th
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
Wednesday, April the 20th
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 ! Applications: communication protocols, cryptographic protocols, reconfigurable systems, biological systems, . . . .
Jérôme Feret
3
Wednesday, April the 20th
Outline We design abstract semantics: sound,automatic,decidable, butapproximate(indecidability).
Our approach is model-independent: 1. design of aMETA-language; 2. design of static analysis at the level of theMETA-language.
Three family of analyses: 1. static analysis ofthe dynamic links between components: (confinment,confidentiality. . ), . 2.counting the number of components: (mutual exclusion,non-exhaustion of resources. . ), . 3. static analysis of computation units: (race detection,authentication,update integrity,. . . ).
Jérôme Feret
4
Wednesday, April the 20th
Static analysis of the dynamic links between components Which components may interact with each other?
client creation
clients
server instances
server
The analysis distinguishes between recursive components Abstract domain:relations among words. Publications: Feret — SAS'00, SAS'01, ESOP'02, JLAP'05
Jérôme Feret
5
Wednesday, April the 20th
Jérôme Feret
6
Static analysis of the number of component Bound the number of components
instances du serveur
clients
Wednesday, April the 20th
création des clients
Abstract domain:numerical relations (affine and interval invariants). Publication : Feret — GETCO'00, JLAP'05
serveur deux ports
client rouge en attente...
Thread partitioning
Idea: gather components in computation units, =thanks to the analysis of linkage between components ; count the number of components within each computation unit, =thanks to the occurrence counting analysis. Advantage: each session is isolated,
which enables the analysisto focus to each session.
Jérôme Feret
7
Wednesday, April the 20th
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
Wednesday, April the 20th
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
Wednesday, April the 20th
Jérôme Feret
Dynamic linkage of agents
A

C
10

B

Wednesday, April the 20th
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