CONPASU tool

CONPASU-tool (CONcurrent Process Analysis SUpport tool)

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.

2. Introduction

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)

Fig.1. A screen shot of CONPASU-tool
...

4. Example

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

Last modified: 12 October 2012