62 Pages
English
Gain access to the library to view online
Learn more

Analysis of Mobile Systems by Abstract Interpretation

-

Gain access to the library to view online
Learn more
62 Pages
English

Description

Niveau: Supérieur, Doctorat, Bac+8
Soutenance de thèse Analysis of Mobile Systems by Abstract Interpretation Jérôme Feret École Normale Supérieure feret February 2005

  • abstract interpretation

  • design analyses

  • between recursive

  • abstract interpretation theory

  • process creation

  • interactions control

  • mobile systems

  • capture dynamic

  • link between


Subjects

Informations

Published by
Reads 4
Language English

Exrait

Soutenance de thèse
Analysis of Mobile Systems by Abstract Interpretation
Jrôme Feret École Normale Suprieure http://www.di.ens.fr/feret
February 2005
Introduction I
We propose aunifying frameworkto design automatic, sound, approximate, decidable, semanticsto abstract the properties of mobile systems.
Our framework ismodel-independent: =we use aMETA-languageto encode mobility models, =we design analysesat theMETA-language level.
We use theAbstract Interpretationtheory.
Jérôme Feret, LIENS
2
February 2005
Introduction II
We focus onreachability properties. Wedistinguish between recursive instancesof components.
We design three families of analyses: 1. environment analyses capturedynamic topology properties (non-uniform control flow analysis,secrecy,confinement,. . .) 2. occurrence counting capturesconcurrency properties (mutual exclusion,non exhaustion of resources) 3.thread partitioningmixes both dynamic topology and concurrency prop-erties (absence of race conditions,authentication,. . .).
Jérôme Feret, LIENS
3
February 2005
Overview
1.Mobile systems 2. Theπ-calculus 3. Abstract Interpretation 4. Environment analyses 5. Occurrence counting analysis 6. Thread partitioning 7. Conclusion
Jérôme Feret, LIENS
4
February 2005
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, LIENS
5
February 2005
Jérôme Feret, LIENS
client
add, query
client
add, query
client
answer
A connection
6
server
server
add, query
server
answer
February 2005