J. Feret, Ph.D. defense

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

PhD advisor

M. Patrick Cousot

President

M. David Schmidt

Reviewers

M. Luca Cardelli
M. David Schmidt

Examiners

M. Vincent Danos
M. Roberto Giacobazzi
M. Jean Goubault-Larrecq

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 on HAL: https://theses.hal.science/pastel-00001303

Slides

Slides of the 45mn presentation are available in various format:
- postscript (ps)
- compressed postscript (ps.gz)
- portable document (pdf)
Slides of the presentation at PPS concurrency working group

First session 10/03/2005

postscript (ps)
compressed postscript (ps.gz)
portable document (pdf)

Second session 31/03/2005

postscript (ps)
compressed postscript (ps.gz)
portable document (pdf)

Third session 16/06/2005

postscript (ps)
compressed postscript (ps.gz)
portable document (pdf)

Photos

Natacha's Photos

Xavier's Photos

David's Photos

Prototypes

Prototypes are available on gitlab

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))

Example 2.1.1: ftp server

Example 2.1.2: token ring

Example 2.2.4: toy example

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))

Example 3.1.1: ftp server (in ambients)

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.

Example 8.2.6: ftp server

Example 8.2.7: token ring

Example 8.2.8: server (in ambients)

Example 8.2.11: causality

analysis input
analysis output (uniform analysis)
analysis output (non uniform analysis)

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.