Occurrence counting analysis for the pi-calculus

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.
Type de document :
Communication dans un congrès
GEometry and Topology in COncurrency theory (Satellite Workshop from CONCUR 2000), Aug 2000, University Park, United States. Elsevier, 39(2), pp.1--18, 2001, Electronic Notes in Theoretical Computer Science. 〈10.1016/S1571-0661(05)01155-2〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00527933
Contributeur : Jérôme Feret <>
Soumis le : mercredi 20 octobre 2010 - 16:11:26
Dernière modification le : mardi 24 avril 2018 - 17:20:12

Lien texte intégral

Identifiants

Collections

Citation

Jérôme Feret. Occurrence counting analysis for the pi-calculus. GEometry and Topology in COncurrency theory (Satellite Workshop from CONCUR 2000), Aug 2000, University Park, United States. Elsevier, 39(2), pp.1--18, 2001, Electronic Notes in Theoretical Computer Science. 〈10.1016/S1571-0661(05)01155-2〉. 〈inria-00527933〉

Partager

Métriques

Consultations de la notice

66