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.

Publications

10 25 50
publication icon
Boulgakov A. (2014) Computing maximal bisimulations in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

publication icon
Gibson-Robinson T (2015) NASA Formal Methods

publication icon
Gibson-Robinson T (2015) FDR3: a parallel refinement checker for CSP in International Journal on Software Tools for Technology Transfer

publication icon
Mazur T (2014) CSP-based counter abstraction for systems with node identifiers in Science of Computer Programming

publication icon
Mazur T (2012) A type reduction theory for systems with replicated components in Logical Methods in Computer Science

publication icon
Ouaknine J (2013) A Static Analysis Framework for Livelock Freedom in CSP in Logical Methods in Computer Science

 
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/