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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2008.77

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.77REFERENCES

- [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.- [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.- [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.- [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.- [25] H. Lin, “Symbolic Bisimulation and Proof Systems for the $\pi$ -Calculus,” technical report, School of Cognitive and Computer Science, Univ. of Sussex, 1994.
- [28] A. Ingólfsdóttir and H. Lin, “A Symbolic Approach to Value-Passing Processes,”
Handbook of Processes Algebra, chapter 7, Elsevier, 2001.- [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.
- [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.- [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.- [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.- [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. |