UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Model Checking Probabilistic and Stochastic Extensions of the Pi-calculus

Norman, G; Palamidessi, C; Parker, D; Wu, P; (2009) Model Checking Probabilistic and Stochastic Extensions of the Pi-calculus. IEEE Transactions on Software Engineering , 35 (2) 209 - 223. 10.1109/TSE.2008.77.

Full text not available from this repository.

Abstract

We present an implementation of model checking for probabilistic and stochastic extensions of the pi-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 pi-calculus model checker MMC, we first show an automated procedure for constructing the underlying semantic model of a probabilistic or stochastic pi-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 pi-calculus literature.

Type: Article
Title: Model Checking Probabilistic and Stochastic Extensions of the Pi-calculus
DOI: 10.1109/TSE.2008.77
Keywords: Model Checking, Quantitative Verification, Probabilistic Processes, Stochastic Processes, Pi-calculus
UCL classification: UCL > School of BEAMS > Faculty of Engineering Science > Computer Science
URI: http://discovery.ucl.ac.uk/id/eprint/173253
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item