Skip to Main content Skip to Navigation

Analyse des systèmes mobiles par interprétation abstraite.

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 a unifying framework to discover and prove automatically and statically some properties of mobile systems. We propose a metalanguage to encode the most current models for mobility (the p-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 a-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 clientsever 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.
Document type :
Complete list of metadatas

Cited literature [77 references]  Display  Hide  Download
Contributor : Ecole Polytechnique <>
Submitted on : Tuesday, July 27, 2010 - 2:04:09 PM
Last modification on : Wednesday, October 14, 2020 - 3:57:52 AM
Long-term archiving on: : Thursday, October 28, 2010 - 11:16:14 AM


  • HAL Id : pastel-00001303, version 1



Jérôme Feret. Analyse des systèmes mobiles par interprétation abstraite.. Informatique mobile. Ecole Polytechnique X, 2005. Français. ⟨pastel-00001303⟩



Record views


Files downloads