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's usage with examples from the model. The tool'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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com