Details of Grant 

EPSRC Reference:	EP/E035590/1
Title:	CSP Model Checking: New Technology and Techniques
Principal Investigator:	Roscoe, Professor A
Other Investigators:	Ouaknine, Professor J Lowe, Professor G
Researcher Co-Investigators:
Project Partners:	Formal Systems (Europe) Ltd UNU Institute for Software Technology Verum Consultants BV
Department:	Computer Science
Organisation:	University of Oxford
Scheme:	Standard Research
Starts:	01 May 2007	Ends:	31 October 2011	Value (£):	648,435
EPSRC Research Topic Classifications:	Fundamentals of Computing Software Engineering
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:
Panel History:
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.ox.ac.uk