@InProceedings{Goldsmith04, title = "{CSP}: {T}he {B}est {C}oncurrent-{S}ystem {D}escription {L}anguage in the {W}orld - {P}robably!", author= "Goldsmith, Michael", editor= "East, Ian R. and Duce, David and Green, Mark and Martin, Jeremy M. R. and Welch, Peter H.", pages = "227--232", booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2004", isbn= "1 58603 458 8", year= "2004", month= "sep", abstract= "CSP, Hoare's Communicating Sequential Processes, is one of the formalisms that underpins the antecedents of CPA, and this year celebrates its Silver Jubilee. Formal Systems' own FDR refinement checker is among the most powerful explicit exhaustive finite-state exploration tools, and is tailored specifically to the CSP semantics. The CSPm ASCII form of CSP, in which FDR scripts are expressed, is the de-facto standard for CSP tools. Recent work has experimentally extended the notation to include a probabilistic choice construct, and added functionality into FDR to produce models suitable for analysis by the Birmingham University PRISM tool." }