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 three areas: 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.