about this paperpresentation abstract bibitemdownloadsslides paper (on HAL) editor link |
Abstract:
We propose an abstract interpretation-based analysis for
automatically proving non-trivial properties
of mobile systems of processes. We focus on properties relying on
the number of occurrences of processes during
computation sequences, such as mutual exclusion and non-exhaustion of
resources.
We design a non-standard semantics for the pi-calculus
in order to explicitly trace the origin of channels and
to solve efficiently problems set by alpha-conversion and
non-deterministic choices. We abstract this semantics into an approximate one.
The use of a relational domain for counting the occurrences of processes
allows us to prove quickly and
efficiently properties such as mutual exclusion and non-exhaustion
of resources. The results obtained are to the best of our knowledge
much more precise than those obtained with other published analyses for mobile systems. At last, dynamic partitioning allows us to detect
some configurations by which no infinite computation sequences can pass.
@article{feret:occurrence-counting,
author = "J{\'e}r{\^o}me Feret",
title = "Occurrence Counting Analysis for the pi-Calculus",
journal = "Electronic Notes in Theoretical Computer Science",
year = "2001",
volume = "39.(2)",
note = "Workshop on GEometry and Topology in COncurrency
theory, PennState, USA, August 21, 2000"
}