Model checking the probabilistic pi-calculus

Gethin Norman 1 Catuscia Palamidessi 2 David Parker 1 Peng Wu 2
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 the probabilistic pi-calculus, a process algebra which supports modelling of concurrency, mobility and discrete probabilistic behaviour. Formal verification techniques for this calculus have clear applications in several domains, including mobile ad-hoc network protocols and random security protocols. Despite this, no implementation of automated verification exists. Building upon the (non-probabilistic) pi-calculus model checker MMC, we first show an automated procedure for constructing the Markov decision process representing a probabilistic pi-calculus process. This can then be verified using existing probabilistic model checkers such as PRISM. Secondly, we demonstrate how for a large class of systems a more efficient, compositional approach can be applied, which uses our extension of MMC on each parallel component of the system and then translates the results into a highlevel model description for the PRISM tool. The feasibility of our techniques is demonstrated through three case studies from the pi-calculus literature.
Type de document :
Communication dans un congrès
4th International Conference on the Quantitative Evaluation of SysTems (QEST), Sep 2007, Edinburgh, United Kingdom. IEEE Computer Society, pp.169-178, 2007, 〈10.1109/QEST.2007.27〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00201069
Contributeur : Catuscia Palamidessi <>
Soumis le : dimanche 23 décembre 2007 - 01:15:58
Dernière modification le : jeudi 10 mai 2018 - 02:06:31
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 13:21:17

Fichier

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

Identifiants

Collections

Citation

Gethin Norman, Catuscia Palamidessi, David Parker, Peng Wu. Model checking the probabilistic pi-calculus. 4th International Conference on the Quantitative Evaluation of SysTems (QEST), Sep 2007, Edinburgh, United Kingdom. IEEE Computer Society, pp.169-178, 2007, 〈10.1109/QEST.2007.27〉. 〈inria-00201069〉

Partager

Métriques

Consultations de la notice

222

Téléchargements de fichiers

124