Lazy Exploration and Checking of CSP Models with CSPsim

Research output: Contribution to conferencePaper

Standard

Lazy Exploration and Checking of CSP Models with CSPsim. / Brooke, Phillip J.; Paige, Richard F.

2007. 33-49 Paper presented at 30th Communicating Process Architectures , Guildford, Surrey, United Kingdom.

Research output: Contribution to conferencePaper

Harvard

Brooke, PJ & Paige, RF 2007, 'Lazy Exploration and Checking of CSP Models with CSPsim' Paper presented at 30th Communicating Process Architectures , Guildford, Surrey, United Kingdom, 8/07/07 - 11/07/07, pp. 33-49.

APA

Brooke, P. J., & Paige, R. F. (2007). Lazy Exploration and Checking of CSP Models with CSPsim. 33-49. Paper presented at 30th Communicating Process Architectures , Guildford, Surrey, United Kingdom.

Vancouver

Brooke PJ, Paige RF. Lazy Exploration and Checking of CSP Models with CSPsim. 2007. Paper presented at 30th Communicating Process Architectures , Guildford, Surrey, United Kingdom.

Author

Brooke, Phillip J. ; Paige, Richard F. / Lazy Exploration and Checking of CSP Models with CSPsim. Paper presented at 30th Communicating Process Architectures , Guildford, Surrey, United Kingdom.

Bibtex - Download

@conference{23f676906894470eafa5d45bbafc89ca,
title = "Lazy Exploration and Checking of CSP Models with CSPsim",
abstract = "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.",
author = "Brooke, {Phillip J.} and Paige, {Richard F.}",
note = "isbn: 978-1-58603-767-3; 30th Communicating Process Architectures ; Conference date: 08-07-2007 Through 11-07-2007",
year = "2007",
language = "English",
pages = "33--49",

}

RIS (suitable for import to EndNote) - Download

TY - CONF

T1 - Lazy Exploration and Checking of CSP Models with CSPsim

AU - Brooke, Phillip J.

AU - Paige, Richard F.

N1 - isbn: 978-1-58603-767-3

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

M3 - Paper

SP - 33

EP - 49

ER -