CSP Model Checking: New Technology and Techniques
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
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.
Organisations
- University of Oxford (Lead Research Organisation)
- D-RisQ (Collaboration)
- Formal Systems (Europe) Ltd. (Collaboration)
- Qinetiq (United Kingdom) (Collaboration)
- Formax (Collaboration)
- Draper Laboratory (Collaboration)
- United Nations University Institute on Computing and Society (Project Partner)
- Formal Systems (Europe) Ltd (Project Partner)
- Verum Consultants BV (Project Partner)
Publications
Boulgakov A
(2014)
Formal Methods and Software Engineering
Brookes S
(2021)
Theories of Programming - The Life and Works of Tony Hoare
Gibson-Robinson T
(2015)
FDR3: a parallel refinement checker for CSP
in International Journal on Software Tools for Technology Transfer
Gibson-Robinson T
(2014)
Tools and Algorithms for the Construction and Analysis of Systems
Khattri M
(2011)
Translating Timed Automata to Tock-CSP
Mazur T
(2014)
CSP-based counter abstraction for systems with node identifiers
in Science of Computer Programming
Mazur T
(2012)
A type reduction theory for systems with replicated components
in Logical Methods in Computer Science
Mazur Tomasz Krzysztof
(2011)
Model Checking Systems with Replicated Components using CSP
Mestel D
(2020)
Translating between models of concurrency
in Acta Informatica
Ouaknine J
(2011)
CONCUR 2011 - Concurrency Theory
Ouaknine J
(2013)
A Static Analysis Framework for Livelock Freedom in CSP
in Logical Methods in Computer Science
Palikareva H
(2012)
SAT-solving in CSP trace refinement
in Science of Computer Programming
Palikareva Hristina
(2012)
Techniques and tools for the verification of concurrent systems
Roscoe A
(2013)
Checking noninterference in Timed CSP
in Formal Aspects of Computing
| Description | We experimented with a variety of potential modifications to CSP, both novel and based on techniques used in other tools. In summary: SAT checking as a way of implementing FDR's general check: worked but by and large not as well as our previous techniques SAT checking for specialised analysis based on local information derived from networks: worked well for divergence freedom. Counter Analysis: worked well for some classes of system. Real time: Timed CSP now incorporated into FDR and works well. CEGAR: works but needs further development. |
| Exploitation Route | They have been taken forward substantially by us on follow-on funding and used in industry. |
| Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy,Manufacturing, including Industrial Biotechology,Security and Diplomacy,Transport |
| Description | As detailed under "Collaborations" our research has been used substantially by industry and led to two REF 2014 case studies. |
| First Year Of Impact | 2014 |
| Sector | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Healthcare,Security and Diplomacy |
| Impact Types | Economic,Policy & public services |
| Description | Centre for Defence Enterprise |
| Amount | £55,568 (GBP) |
| Funding ID | CDE 23010 |
| Organisation | Defence Science & Technology Laboratory (DSTL) |
| Department | Centre for Defence Enterprise |
| Sector | Public |
| Country | United Kingdom |
| Start | 12/2011 |
| End | 04/2012 |
| Description | Centre for Defence Enterprise |
| Amount | £55,568 (GBP) |
| Funding ID | CDE 23010 |
| Organisation | Defence Science & Technology Laboratory (DSTL) |
| Department | Centre for Defence Enterprise |
| Sector | Public |
| Country | United Kingdom |
| Start | 12/2011 |
| End | 04/2012 |
| Description | Participation in the HACMS programme |
| Amount | $1,292,000 (USD) |
| Organisation | Defense Advanced Research Projects Agency (DARPA) |
| Sector | Public |
| Country | United States |
| Start | 07/2012 |
| End | 01/2017 |
| Description | ASD |
| Organisation | Formax |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Verum used FDR as the verification back end of their ASD embedded software tool. We provided technical support on FDR and customised versions of FDR |
| Collaborator Contribution | Research problems based on practice |
| Impact | See case study at URL above |
| Description | Collaboration with QinetiQ/D-RisQ |
| Organisation | D-RisQ |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | D-RisQ is a spin-out of QinetiQ which consists of the team that we formerly collaborated with there. They have long been big users of FDR, and we assist them in this |
| Collaborator Contribution | Bringing research problems and practical applications |
| Impact | See impact case study referenced above |
| Description | Collaboration with QinetiQ/D-RisQ |
| Organisation | Qinetiq |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | D-RisQ is a spin-out of QinetiQ which consists of the team that we formerly collaborated with there. They have long been big users of FDR, and we assist them in this |
| Collaborator Contribution | Bringing research problems and practical applications |
| Impact | See impact case study referenced above |
| Description | Draper |
| Organisation | Draper Laboratory |
| Country | United States |
| Sector | Charity/Non Profit |
| PI Contribution | Draper are substantial users of FDR, generally in projects related to the US Military. We advise them on this use. |
| Collaborator Contribution | Practical problems driving FDR development It is through Draper that we obtained nearly $1.3M DARPA funding to develop FDR3 and its use. |
| Impact | FDR has been employed by Draper to verify several pieces of US Military hardware, for example for the Navy. The details of this work are classified or confidential. |
| Description | Formal Systems |
| Organisation | Formal Systems (Europe) Ltd. |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Our work was licenced back to Formal Systems |
| Collaborator Contribution | Formal Systems developed all versions of FDR up to 2008. They transferred their code and the right to develop to the university at the start of the EPSRC grant that started then |
| Impact | Formal Systems handles all commercial licencing of FDR2 and FDR3, with a revenue split between it and the university. |
| Title | FDR |
| Description | FDR is a model checker for CSP. It has been developed continuously since 1991, with FDR2 released in 1996 and FDR3 in 2011. Parts of it are open source. Parts of FDR2 were developed under EPSRC funding; FDR3 has mainly been developed as a successor under DARPA funding. |
| Type Of Technology | Software |
| Year Produced | 2011 |
| Impact | Used by organisations including DERA/QinetiQ, Verum and its customers, Draper Labs, Praxis, IBM, AWE and NSA. For major ones see "collaborations" |
| URL | https://www.cs.ox.ac.uk/projects/fdr/ |