%T Lazy Exploration and Checking of CSP Models with CSPsim
%A Philip J Brooke, Richard F. Paige
%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
If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.
Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.
Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org