Professor Bill Roscoe FREng
Professor of Computing Science
Senior Research Fellow, University College
- Concurrency: this is the study of how systems interact by communication when operating in parallel. Most of my work is done on the process algebra CSP (or Communicating Sequential Processes) originally introduced by Tony Hoare. This is a relatively mature area (I have worked on it since beginning my own doctoral work in 1978) but it still throws up new surprises and insights: for example relatively recently I discovered ways to prove that some of the models that have been studied for many years are in some sense Platonic: they underly every possible model. The work I do under this category is largely theoretical, but it underpins many of the more practical topics below. My work on CSP divides into two parts: the original untimed CSP where we worry about the order of events but not about exactly when they each happen, and timed versions such as Timed CSP, which I developed with Mike Reed and has a continuous time model, and various discrete models.
- Verification: this is the study of how to prove that systems meet their specification, and these days is almost always done or much assisted by verification tools: programs that analyse other programs, usually comparing them against some specification. Most of my own work in this area is based on, or related to, CSP and its refinement checker FDR (see below). My work on verification breaks down into actually doing practical verification and developing methods that make it easier or more powerful. I've enjoyed working with industry over the years to help them with specific verifications, especially inmos (in former times) and QinetiQ. I'm interested in induction, data independence, their combination, and similar ideas to help generalise verification (and in particular model checking) from something that can only be done for a very specific system to something that can prove results about classes of them.
- FDR (standing for Failures Divergence Refinement) is a verification tool for CSP. What it primarily does is discover if one CSP program refines another, namely has less possible observations that can be made of it. Thus refinement essentially coincides with reduction of nondeterminism. FDR is a model checker, but an unusual one because it concentrates on refinement. It has a wide user base in academia, government and industry, both as a tool in itself and also as the "back end" to others. I have led its design since it was first written in 1991. We recently had funding from EPSRC to look, amongst other things, at how we can include modern model checking ideas such as SAT checking into it: for results see paper 150. I am interested in improving how FDR works, in developing ways of using it effectively (for example on real-time systems), and in finding ways of verifying non-CSP notations such as Statecharts with it. A current interest is investigating what types of language can, in principle, be translated into CSP (see paper 125) We have relatively recently added Timed CSP into FDR, giving its role in modelling real-time systems a new impetus: see papers 145, 149, 150. Recently, a new and vastly improved version of this called FDR3 was released, developed mainly by Tom Gibson-Robinson. Our group is actively exploring how to make FDR more efficient, giving it new capabilities and finding new ways of applying it.
- SVA is a front end for FDR that analyses shared variable programs, developed by me and David Hopkins. It is described in Chapters 18 and 19 of Understanding Concurrent Systems.
- Computer Security: I became interested in this in the mid 1990's when I saw the successes other people were having applying the ideas of CSP. I work on three different topics in security. Noninterference is the study of how information might either leak, or be shown not to leak, from one user to another across a computer system. Understanding this is a real challenge and is perhaps the most convincing application of the finer theoretical details of concurrency theory: it is very easy to come up with convincing looking specifications of noninterference that are wrong. I concentrate on the idea that a system S is free of information leakage from A to B if, after suitably abstracting A's behaviour in S, the resulting view (B's) is either deterministic or perhaps maximally refined. I have two big goals in this area: finding a way of expressing noninterference elegantly for stochastic systems (the main desideratum being a model that mixes nondeterminism and probability at the right level of abstraction) and finding real practical applications for our noninterference work - it can readily be checked on FDR. Cryptographic protocol analysis is the study of how to analyse protocols that use cryptography to achieve results like key exchange, authentication and secure e-commerce. We do not study the mathematical details of the underlying cryptography, which is modelled symbolically. Gavin Lowe realised in 1994 that these protocols could be modelled and analysed on FDR and, ever since then, he, I and our co-workers have developed and refined these techniques to the point where they are now robust and widely applicable. A spin-off of this work my development of protocols and related cryptography for bootstrapping ad hoc networks. Here we develop methods for securely building secure networks between pairs or larger groups of systems based not on traditional methods such as PKIs, but on a minimum of non-fakable human interaction (either just human-machine, or a mixture of human-machine and human-human). Applications of this include medical data exchange, secure telephony and improved credit card security: see below. Principles derived from this work have recently enabled us to develop more efficient forms of cryptographic signature. This novel view of how to do authentication leads to a new cryptographic primitive: the keyed digest function. I am interested in discovering more about these and developing them so they can be computed efficiently and confidently.
In the past I've also worked on general topology, digital topology and hardware verification, but these are not current areas.
I enjoy collaborating with industry, particularly users of my own research.
Mobile security technology
We have built prototypes of the ad hoc bootstrapping technology referred to above. This technology is being developed by OxCept, a spin-out company founded specially for this purpose.
Prospective Research Students
In principle I'm interested in taking on research students interested in any of these areas, but obviously I am likely to have some more specific projects in mind at any given moment. Please email me if you are interested in becoming my research student.
Published in October 2010 by Springer, this book provides an up-to-date introduction to CSP, its theory and applications, including the use of CSP to give semantics for, and generate tools for, other models of concurrent systems.
Bill Roscoe (Andrew William, hence A.W. Roscoe on papers) was born and brought up in Dundee, Scotland. He read Mathematics at University College, Oxford (Univ) 1975-78, obtaining the top mark for his year in the university. Together with another Univ student, Steve Brookes (now at CMU), he joined the Computing Laboratory (PRG) as a research student in 1978, and their DPhil work with Tony Hoare was on the mathematical foundations and models of his Communicating Sequential Processes (CSP) process algebra. Almost all Bill's subsequent research has either been based on CSP or has been a spin-off from it (examples of the latter being Hardware Verification and Computer Security). He was a Junior Research Fellow of St Edmund Hall 1980-3 and a Royal Society Research Fellow 1982-3. He became a College Lecturer at Univ in 1979 and a Tutorial Fellow there in 1983, when he was also appointed a University Lecturer in Computer Science at Oxford. He was given the title of Professor in 1997. In 2007 his job title was changed to "Research Professor" and he became a Senior Research Fellow at Univ. In 1993-7 he was Senior Tutor of Univ, in 1998-2000 he was the last ever Chairman of the Mathematical Sciences Faculty Board, and was Head of the Department of Computer Science (formerly called Director of the Computing Labratory) 2003-8 and 2009-14.
FDR3: a parallel refinement checker for CSP
Thomas Gibson−Robinson‚ Philip Armstrong‚ Alexandre Boulgakov and A.W. Roscoe
In International Journal on Software Tools for Technology Transfer. 2015.
Practical partial order reduction for CSP
A.W. Roscoe T. Gibson−Robinson H. Hansen and X Wang
In NASA Formal Methods‚ 2015. 2015.
The expressiveness of CSP with priority
In Proceedings of MFPS 2015. 2015.