[moca] PhD thesis: Analysis of mobile systems by abstract interpretation

[Jerome Feret <Jerome.Feret@xxxxxx>]

Dear all,

I am pleased to announce that my PhD thesis "Analysis of mobile systems" 
is available at :

   http://www.di.ens.fr/~feret/thesis/thesis.pdf

Comments are welcome.
Best regards.


Here is the abstract of the thesis:

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 a 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 
bioambients, 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.

   Then, we 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-sever 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 unit. Then, it 
abstract the number of occurrence of agent 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.

-------------------------

Jerome Feret, 
Ecole Normale Superieure 
Departement d'Informatique 
45 rue d'Ulm, 
75 230 Paris Cedex 05 
01 44 32 37 66 
feret@xxxxxx

 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html