@InProceedings{MartinJassim97b, title = "{H}ow to {D}esign {D}eadlock-{F}ree {N}etworks {U}sing {CSP} and {V}erification {T}ools -- {A} {T}utorial {I}ntroduction", author= "Martin, Jeremy M. R. and Jassim, S. A.", editor= "Bakkers, Andr\`{e} W. P.", pages = "326--338", booktitle= "{P}roceedings of {W}o{TUG}-20: {P}arallel {P}rogramming and {J}ava", isbn= "90 5199 336 6", year= "1997", month= "mar", abstract= "The CSP language of C.A.R. Hoare originated as a blackboard mathematical notation for specifying and reasoning about parallel and distributed systems. More recently sophisticated tools have emerged which provide automated verification of CSP-specified systems. This has led to a tightening and standardisation of syntax. This paper outlines the syntax and semantics of CSp as it is now used and then describes how to design CSP networks, which are guaranteed to be free of deadlock, throught a succession of increasingly complex worked examples, making use of the verification tool Deadlock Checker." }