Analysis of Mobile Systems by Abstract Interpretation

Jérôme Feret

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

Sujets

• Abstract interpretation

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 4
• Langue: English

Extrait

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 a META -languageto encode mobility models, =⇒we design analysesat the META -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