This page is still under
construction.

CONPASU-tool is a fully automatic analysis tool for concurrent processes based on symbolic computation.

1. News

- (12/10/2012) A publication and some links were added.

- (31/03/2011) This web-site was opened.

CONPASU is an implementation of analysis-tool for concurrent processes with value-passing which may cause infinite-state systems. The method consists of two steps: sequentialization and state-reduction. In the sequentialization, the symbolic transition graph of a given concurrent process is derived by symbolic operational semantics. In the state-reduction, the number of states in the symbolic transition graph is reduced by removing needless internal transitions. For example, CONPASU can extract abstract behaviors, which are useful for understanding complex behaviors, by focusing on some interesting events.

3. Download

- Proof note for
CONPASU-tool : (to be avaiable soon)

- A prototype of CONPASU-tool : (to be avaialble soon)

- ...

5. Publication

- Yoshinao Isobe, Yutaka Oiwa, Koichi Takahashi, and Kiyoshi
Tanaka, An Analysis Support Tool for Concurrent Systems --
Visualization of Concurrent Behavior --, 10th WOCS2 (10th Workshop of Critical Software System), 2012. [slide written in Japanese (PDF, 2.7MB)]

- Yoshinao Isobe, CONPASU-tool: A Concurrent Process
Analysis Support Tool based on Symbolic Computation, CPA 2011 (Communicating
Process Architectures 2011, the 33rd WoTUG conference on concurrent and parallel programming), IOS Press, pp.341-362, Ireland,
June 2011. [paper (PDF, 0.5MB), slides (PDF, 3.0MB)]

- Yoshinao
Isobe, CONPASU-tool: A Prototype of a Concurrent Process Analysis
Support Tool based on Symbolic Computation (written in Japanese), FOSE
2010 (17th Workshop on Foundation of
Software Engineering), Japanese
Lecture Notes Series 36, Kindai-kagaku-sha, pp.65-74, 2010. [slides (PDF, 3.4MB)]

6. Link

- Tools for CSP, etc.

- CSP-Prover
: a theorem prover for CSP

- FDR : a model
checker for CSP

- PAT : a model checker for CSP
- ProB : a model
checker for CSP and B

- mCRL
: a model checker for a process algebra (ACP)

- LTSA : a labeled
transition system analyzer

- CWB : a
model checker for CCS

- MWB
: a model checker for pi-calculus

- Textbooks for CSP

- C. A. R. Hoare, Communicating Sequential Processes (PDF), Prentice Hall, 1985.
- A. W. Roscoe, The Theory and Practice of Concurrency (PDF), Prentice Hall, 1997.
- A. W. Roscoe, Understanding Concurrent Systems, Springer, 2011.
- S. Schneider, Concurrent and Real-time Systems: The CSP Approach (PDF), John Wiley & Sons, Inc., 1999.

7. Contact

Yoshinao Isobe

Information Technology Research Institute

National Institute of Advanced Industrial Science and Technology (AIST)

Tsukuba Central 2, 1-1-1, Umezono, Tsukuba, Ibaraki, 305-8568, Japan

Information Technology Research Institute

National Institute of Advanced Industrial Science and Technology (AIST)

Tsukuba Central 2, 1-1-1, Umezono, Tsukuba, Ibaraki, 305-8568, Japan

Last modified: 12 October 2012