The Community for Technology Leaders
Green Image
Issue No. 02 - March/April (2009 vol. 35)
ISSN: 0098-5589
pp: 209-223
Catuscia Palamidessi , INRIA Saclay and École Polytechnique, Paris
Peng Wu , University College London, Ipswich
David Parker , Oxford University, Oxford
Gethin Norman , Oxford University, Oxford
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 π-calculus literature.
INDEX TERMS
Model checking, Markov processes, Stochastic processes
CITATION
Catuscia Palamidessi, Peng Wu, David Parker, Gethin Norman, "Model Checking Probabilistic and Stochastic Extensions of the π-Calculus", IEEE Transactions on Software Engineering, vol. 35, no. , pp. 209-223, March/April 2009, doi:10.1109/TSE.2008.77
90 ms
(Ver )