CSP Model Checking: New Technology and Techniques
Concurrency is becoming increasingly important, both to overcome limitations in processor speed, and to allow distributed
transactions in an increasingly networked world. Message passing is widely considered to be the most appropriate model for
concurrency. The overall aim of this project is to improve techniques for reasoning about concurrency based on message passing.
The process algebra CSP has been widely used for the verification of concurrent systems, most notably in the area of computer
security and hardware design. The model checker FDR can be used to analyse concurrent systems modelled in CSP.
The proposed research aims to improve tools and techniques for performing such analyses. In particular, work will focus in
1. Improvements in model checking technology, via enhancements to the FDR tool, with lessons for other tools;
2. Techniques for analysing parameterised systems (in particular systems that are parameterised by the number of components)
so as to verify the correctness of the system for all values of the parameter;
3.Improved techniques for modelling and analysing timed systems.