WoTUG - The place for concurrent processes

Paper Details


%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
   systems.


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

Valid HTML 4.01!