Case studies with probabilistic CSP
|
Supervisor |
|
|
Suitable for |
Abstract
A recent extension of the FDR model checker for CSP concerns probability. Probabilistic processes are translated into input for the Prism tool, which will then give the probability ---or rather probabilities; there may be a range, because of nondeterminism--- with which the process acts like a particular specification.
The aim of this project would be to carry out case studies using this extension, and so to build up experience in modelling and analysing probabilistic systems. Possible subjects for these case studies would include:
- sensor networks (where nodes can be probabilistically captured by an attacker);
- protocols that aim to be resistant to denial of service attacks;
- fault-tolerant systems (where the faults occur probabilistically, and the system aims to overcome those faults);
- probabilistic algorithms (where the algorithm uses probability, typically to help break symmetry).
The Concurrency course would be a prerequisite; the Security course would provide useful background for the first two topics.
NOT AVAILABLE IN 2010/11