CONPASU-tool (CONcurrent Process Analysis
This page is still under
a fully automatic analysis tool for concurrent processes based on
- (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.
- Proof note for
CONPASU-tool : (to be avaiable soon)
- A prototype of CONPASU-tool : (to be avaialble soon)
Fig.1. A screen shot of
- 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)]
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)]
- Tools for CSP, etc.
: 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
: a model checker for a process algebra (ACP)
- LTSA : a labeled
transition system analyzer
- CWB : a
model checker for CCS
: 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.
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