loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007)
Model checking the probabilistic pi-calculus
Edinburgh, Scotland, UK
September 17-September 19
ISBN: 0-7695-2883-X
Gethin Norman, Oxford University, England
Catuscia Palamidessi, INRIA Futurs and LIX, Ecole Polytechnique, France
David Parker, Oxford University, England
Peng Wu, CNRS and LIX, Ecole Polytechnique, France
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 high-level model description for the PRISM tool. The feasibility of our techniques is demonstrated through three case studies from the \pi-calculus literature.
Citation:
Gethin Norman, Catuscia Palamidessi, David Parker, Peng Wu, "Model checking the probabilistic pi-calculus," qest, pp.169-178, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.