Subscribe
Issue No.02 - March/April (2009 vol.35)
pp: 209-223
Gethin Norman , Oxford University, Oxford
Catuscia Palamidessi , INRIA Saclay and École Polytechnique, Paris
David Parker , Oxford University, Oxford
Peng Wu , University College London, Ipswich
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
Gethin Norman, Catuscia Palamidessi, David Parker, Peng Wu, "Model Checking Probabilistic and Stochastic Extensions of the π-Calculus", IEEE Transactions on Software Engineering, vol.35, no. 2, pp. 209-223, March/April 2009, doi:10.1109/TSE.2008.77
REFERENCES
 [1] R. Milner, J. Parrow, and D. Walker, “A Calculus of Mobile Processes, I,” Information and Computation, vol. 100, pp. 1-40, 1992. [2] M. Reiter and A. Rubin, “Crowds: Anonymity for Web Transactions,” ACM Trans. Information and System Security, vol. 1, no. 1, pp. 66-92, 1998. [3] S. Even, O. Goldreich, and A. Lempel, “A Randomized Protocol for Signing Contracts,” Comm. ACM, vol. 28, no. 6, pp. 637-647, 1985. [4] O. Herescu and C. Palamidessi, “Probabilistic Asynchronous $\pi$ -Calculus,” Proc. Third Int'l Conf. Foundations of Software Science and Computation Structures, J. Tiuryn, ed., pp. 146-160, 2000. [5] K. Chatzikokolakis and C. Palamidessi, “A Framework to Analyze Probabilistic Protocols and Its Application to the Partial Secrets Exchange,” Proc. Int'l Symp. Trustworthy Global Computing, R.D.Nicola and D. Sangiorgi, eds., pp. 146-162. Springer, 2005. [6] M. Bhargava, C. Palamidessi, “Probabilistic Anonymity,” Proc. 16th Int'l Conf. Concurrency Theory, M. Abadi and L. de Alfaro, eds., pp. 171-185, 2005. [7] C. Priami, “Stochastic $\pi$ -Calculus,” Computer J., vol. 38, no. 7, pp. 578-589, 1995. [8] A. Regev, W. Silverman, and E. Shapiro, “Representation and Simulation of Biochemical Processes Using the $\pi$ -Calculus Process Algebra,” Proc. Pacific Symp. Biocomputing, R. Altman, A. Dunker, L. Hunter, and T. Klein, eds., vol. 6, pp. 459-470, 2001. [9] C. Priami, A. Regev, W. Silverman, and E. Shapiro, “Application of a Stochastic Name Passing Calculus to Representation and Simulation of Molecular Processes,” Information Processing Letters, vol. 80, pp. 25-31, 2001. [10] P. Yang, C. Ramakrishnam, and S. Smolka, “A Logic Encoding of the $\pi$ -Calculus: Model Checking Mobile Processes Using Tabled Resolution,” Int'l J. Software Tools Technology Transfer, vol. 4, pp. 1-29, 2004. [11] A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, “PRISM: A Tool for Automatic Verification of Probabilistic Systems,” Proc. 12th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, H. Hermanns and J. Palsberg, eds., pp. 441-444, 2006. [12] B. Victor and F. Moller, “The Mobility Workbench—A Tool for the $\pi$ -Calculus,” Proc. Sixth Int'l Conf. Computer Aided Verification, R.Alur and D. Peled, eds., pp. 428-440, 1994. [13] B. Blanchet, ProVerif: Automatic Cryptographic Protocol Verifier User Manual, www.preverif.ens.frproverif-manual.ps.gz , 2005. [14] S. Chaki, S. Rajamani, and J. Rehof, “Types as Models: Model Checking Message-Passing Programs,” Proc. 29th Symp. Principles of Programming Languages, pp. 45-57, 2002. [15] P. Wu, “Interpreting $\pi$ -Calculus with Spin/Promela,” Computer Science, vol. 8, pp. 7-9, supplement, 2003. [16] H. Song and K. Compton, “Verifying $\pi$ -Calculus Processes by Promela Translation,” Technical Report CSE-TR-472-03, Univ. of Michigan, 2003. [17] A. Venet, “Abstract Interpretation of the $\pi$ -Calculus,” Proc. Fifth LOMAPS Workshop Analysis and Verification of Multiple-Agent Languages, M. Dam, ed., pp. 51-75, 1996. [18] C. Bodei, P. Degano, F. Nielson, and H.R. Nielson, “Static Analysis for the $\pi$ -Calculus with Applications to Security,” Information and Computation, vol. 165, pp. 68-92, 2001. [19] A. Phillips and L. Cardelli, “Efficient, Correct Simulation of Biological Processes in the Stochastic $\pi$ -Calculus,” Proc. Fifth Int'l Workshop Computational Methods in Systems Biology, M. Calder and S. Gilmore, eds., pp. 184-199, 2007. [20] G. Norman, C. Palamidessi, D. Parker, and P. Wu, “Model Checking the Probabilistic $\pi$ -Calculus,” Proc. Fourth Int'l Conf. Quantitative Evaluation of Systems, pp. 169-178, 2007. [21] R. Milner, Communication and Concurrency. Prentice Hall, 1989. [22] R. Segala and N. Lynch, “Probabilistic Simulations for Probabilistic Processes,” Nordic J. Computing, vol. 2, no. 2, pp. 250-273, 1995. [23] M. Hennessy and H. Lin, “Symbolic Bisimulations,” Theoretical Computer Science, vol. 138, pp. 353-389, 1995. [24] P. Wu, C. Palamidessi, and H. Lin, “Symbolic Bisimulations for Probabilistic Systems,” Proc. Fourth Int'l Conf. Quantitative Evaluation of Systems, pp. 179-188, 2007. [25] H. Lin, “Symbolic Bisimulation and Proof Systems for the $\pi$ -Calculus,” technical report, School of Cognitive and Computer Science, Univ. of Sussex, 1994. [26] M. Boreale and R.D. Nicola, “A Symbolic Semantics for the $\pi$ -Calculus,” Information and Computation, vol. 126, no. 1, pp. 34-52, Apr. 1996. [27] H. Lin, “Complete Inference Systems for Weak Bisimulation Equivalences in the $\pi$ -Calculus,” Information and Computation, vol. 180, no. 1, pp. 1-29, 2003. [28] A. Ingólfsdóttir and H. Lin, “A Symbolic Approach to Value-Passing Processes,” Handbook of Processes Algebra, chapter 7, Elsevier, 2001. [29] J. Hillston, A Compositional Approach to Performance Modelling. Cambridge Univ. Press, 1996. [30] G. Norman, C. Palamidessi, D. Parker, and P. Wu, “Translating the Probabilistic $\pi$ -Calculus to PRISM,” Technical Report CSR-07-02, School of Computer Science, Univ. of Birmingham, 2007. [31] A. Roscoe, The Theory and Practice of Concurrency. Prentice-Hall, 1997. [32] Online PRISM documentation, www.prismmodelchecker.orgdoc/, 2009. [33] H. Hansson and B. Jonsson, “A Logic for Reasoning about Time and Reliability,” Formal Aspects of Computing, vol. 6, no. 5, pp. 512-535, 1994. [34] A. Bianco and L. de Alfaro, “Model Checking of Probabilistic and Nondeterministic Systems,” Proc. 15th Conf. Foundations of Software Technology and Theoretical Computer Science, P.Thiagarajan, ed., pp.499-513, 1995. [35] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, “Verifying Continuous Time Markov Chains,” Proc. Eighth Int'l Conf. Computer Aided Verification, R. Alur and T.Henzinger, eds., pp.269-276, 1996. [36] C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen, “Model-Checking Algorithms for Continuous-Time Markov Chains,” IEEE Trans. Software Eng., vol. 29, no. 6, pp. 524-541, June 2003. [37] M. Goldsmith, N. Moffat, B. Roscoe, T. Whitworth, and I. Zakiuddin, “Watchdog Transformations for Property-Oriented Model-Checking,” Proc. Second Int'l Symp. Formal Methods Europe, K.Araki, S. Gnesi, and D. Mandrioli, eds., pp. 600-616, 2003. [38] L. Caires and L. Cardelli, “A Spatial Logic for Concurrency (PartI),” Information and Computation, vol. 186, no. 2, pp. 194-235, 2003. [39] D. Chaum, “The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability,” J. Cryptology, vol. 1, pp. 65-75, 1988. [40] G. Norman and V. Shmatikov, “Analysis of Probabilistic Contract Signing,” J. Computer Security, vol. 14, no. 6, pp. 561-589, 2006. [41] F. Orava and J. Parrow, “An Algebraic Verification of a Mobile Network,” Formal Aspects of Computing, vol. 4, pp. 497-543, 1992. [42] C. Priami, “Stochastic Analysis of Mobile Telephony Networks,” Proc. Fifth Int'l Workshop Process Algebra and Performance Modeling, E.Brinskma and A. Nymeyer, eds., pp. 145-171, 1997. [43] J. Heath, M. Kwiatkowska, G. Norman, D. Parker, and O. Tymchyshyn, “Probabilistic Model Checking of Complex Biological Pathways,” Proc. Fourth Int'l Workshop Computational Methods in Systems Biology, C. Priami, ed., pp. 32-47, 2006.