Presentation

Presentation Jury Abstract

Download

Thesis Report Slides Photos

Prototypes

Prototypes

Analysis examples

pi-calculus ambient calculus environment analysis occurrence counting analysis thread partitioning

Ph.D. Thesis Defense

Analysis of mobile systems by abstract interpretation


Jérôme Feret


Defended the 25th of February 2005
École Polytechnique

This thesis has been done at Laboratoire d'Informatique of the École Normale Supérieure (Paris)

Jury

Abstract

A mobile system is a pool of agents that may interact with each other. These interactions dynamically change the system by controlling both creation and destruction of links between agents. These interactions also control the creation of new agents. The size of a mobile system evolves during its computation. This size may be unbounded. A mobile system may describe telecommunication networks, reconfigurable systems, client-server applications, cryptographic protocols, or biological systems. Several models are available according to the application field and the granularity of the observation level.

In this thesis, we propose an unifying framework to discover and prove automatically and statically some properties of mobile systems. We propose a meta-language to encode the most current models for mobility (the pi-calculus, the ambients, the join-calculus, the spi-calculus, the bio-ambients, and so on). The meta-language provides an operational semantics for each encoded model. In these semantics, each agent is identified with the history of its creation, so that this semantics avoids the use of alpha-conversion.

We then use the Abstract Interpretation framework to derive abstract semantics, which are sound, decidable, but approximate. In this thesis, we give three generic semantics that we set according to the expected trade-off between accuracy and efficiency. The first analysis focuses on dynamic properties: it captures relations about the creation histories of the agents of the system. This analysis is precise enough to distinguish recursive instances of each agent, even when there is an unbounded number of instances. Thus, we can prove in the case of a client-server application that the server always returns data to the right client. The second analysis focuses on concurrency properties: it counts the number of occurrences of agents inside the system. This analysis detects mutual exclusion and it bounds the number of agents. The third analysis mixes concurrency and dynamic properties. It gathers the agents of the system in several computation units. Then, it abstracts the number of occurrences of agents in each computation unit. For instance, we can prove the absence of race in the specification of a shared-memory with dynamic allocation that is written in the pi-calculus.

PhD. Report

Final version can be downloaded at: http://www.di.ens.fr/~feret/thesis/thesis.pdf

Slides

Photos

Natacha's Photos
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture]
[A picture] [A picture] [A picture] [A picture]
[A picture] [A picture] [A picture] [A picture]
[A picture]
Xavier's Photos
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
David's Photos
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]

Prototypes

Prototypes can be used on line (Computation are made on a Pentium III, 500 MHz, with 128 Mb RAM. There is a time out (after a couple of minutes).

Context-free analysis is only implemented in the pi-calculus analyzer.

Analysis examples

Analysis examples (These results have been computed on a amd Opteron 248, with 8 Gb of RAM)

Chap. 2: the pi-caluclus
Analysis results are computed with default parameters (non-uniform analysis (Loc1) and occurrence counting analysis (distinguishing each kind of transition label / affine equalities + intervals))
Chap. 3: the ambient calculus
Analysis results are computed with default parameters (non-uniform analysis (Loc1) and content analysis (distinguishing each kind of transition label / affine equalities + intervals))
Chap. 8: environment analysis
Only environment analysis is computed, with default parameters (non-uniform analysis (Loc1)). Occurrence counting analysis is disabled. Analyses in Sect 8.3 are not implement yet.
Chap. 9: occurrence counting analysis
Only occurrence counting analysis is computed (with our product between of affine equality domain and interval domain). We partition transtion labels into a linear (with respect to the size of the initial state) number of classes. We also use a uniform control flow analysis.
Chap. 10: thread partitioning
(not implementet yet)
Only implemented for mobile ambients. For the pi-calculus, we give results of environment analysis.