db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>

%T Lazy Exploration and Checking of CSP Models with CSPsim
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
%A  Philip J Brooke,  Richard F. Paige
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
%E  Alistair A. McEwan,  Steve Schneider,  Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X We have recently constructed a model, and carried out an
   analysis, of
a concurrent extension to an object\-oriented
   language at a level of abstraction above threads. The model
   was constructed in CSP. We subsequently found that existing
   CSP tools were unsuitable for reasoning about and analysing
   this model, so it became necessary to create a new tool to
   handle CSP models: CSPsim. We describe this tool, its
   capabilities and algorithms, and compare it with the related
   tools, FDR2 and ProBE. We illustrate CSPsim\[rs]s usage with
   examples from the model. The tool\[rs]s on\-the\-fly
   construction of successor states is important for exhaustive
   and non\-exhaustive state exploration. Thus we found CSPsim
   to be particularly useful for parallel compositions of
   components with infinite states that reduce to finite\-state
   systems.