Model checking probabilistic and stochastic extensions of the $\pi$-calculus

Gethin Norman 1 Catuscia Palamidessi 2, 3 David Parker 1 Peng Wu 4
2 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We present an implementation of model checking for probabilistic and stochastic extensions of the -calculus, a process algebra which supports modelling of concurrency and mobility. Formal verification techniques for such extensions have clear applications in several domains, including mobile ad-hoc network protocols, probabilistic security protocols and biological pathways. Despite this, no implementation of automated verification exists. Building upon the -calculus model checker MMC, we first show an automated procedure for constructing the underlying semantic model of a probabilistic or stochastic -calculus process. This can then be verified using existing probabilistic model checkers such as PRISM. Secondly, we demonstrate how for processes of a specific structure a more efficient, compositional approach is applicable, which uses our extension of MMC on each parallel component of the system and then translates the results into a high-level modular description for the PRISM tool. The feasibility of our techniques is demonstrated through a number of case studies from the pi-calculus literature.
Type de document :
Article dans une revue
IEEE Transactions of Software Engineering, IEEE Computer Society, 2009, 35 (2), pp.209--223
Liste complète des métadonnées

Littérature citée [42 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00424856
Contributeur : Catuscia Palamidessi <>
Soumis le : lundi 19 octobre 2009 - 07:56:06
Dernière modification le : jeudi 10 mai 2018 - 02:06:40
Document(s) archivé(s) le : mardi 16 octobre 2012 - 12:26:56

Fichier

TSE.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00424856, version 1

Collections

Citation

Gethin Norman, Catuscia Palamidessi, David Parker, Peng Wu. Model checking probabilistic and stochastic extensions of the $\pi$-calculus. IEEE Transactions of Software Engineering, IEEE Computer Society, 2009, 35 (2), pp.209--223. 〈inria-00424856〉

Partager

Métriques

Consultations de la notice

364

Téléchargements de fichiers

130