Paper Details

Communicating Process Architectures (CPA)
 Title: De-skilling CSP: Why FDR Needs Lazy Compilation
 Conference: Communicating Process Architectures 2014
 Authors: Bill Roscoe
Department of Computer Science, University of Oxford
 Abstract: Since FDR was first developed in 1991, it has had a huge impact on the way CSP is written. FDR optimises processes that are the parallel combinations of a number of individual processes, each of which is significantly smaller than the size of the overall system we might contemplate checking. Some of the most cunning pieces of CSP coding, most notably the cryptoprotocol intruder, have been created specifically to get around the restrictions this optimal model imposes. In this lecture I will look at the problem of modelling state machines with a few control states but many variables, and will show how if FDR were, instead of compiling all of component processes ab initio, it did so by need, or lazily, we might expect get much simpler CSP scripts for modelling such systems as well as examples such as the intruder. 

BibTeX Entry

Full paper