We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
Model Checking Probabilistic and Stochastic Extensions of the π-Calculus.
- Authors
Norman, Gethin; Palamidessi, Catuscia; Parker, David; Peng Wu
- Abstract
We present an implementation of model checking for probabilistic and stochastic extensions of the π-calculus, a process algebra which supports modeling 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 Mobility 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,
- Subjects
STOCHASTIC processes; SOFTWARE verification; COMPUTER network protocols; COMPUTER simulation; CRYPTOGRAPHY; CALCULUS
- Publication
IEEE Transactions on Software Engineering, 2009, Vol 35, Issue 2, p209
- ISSN
0098-5589
- Publication type
Article
- DOI
10.1109/TSE.2008.77