2010 Fiscal Year Final Research Report
A study on a reliable automatic verification tool for concurrent systems
| Project/Area Number |
20500023
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
ISOBE Yoshinao National Institute of Advanced Industrial Science and Technology, 情報技術研究部門, 主任研究員 (50356458)
|
|---|
| Project Period (FY) |
2008 – 2010
|
| Keywords | 並行システム / プロセス代数 / 自動解析ツール / 記号処理 / 状態数削減 / 無限状態システム / 定理証明器 / モデル検査器 |
|---|
| Research Abstract |
This work aims at developing tools which analyze concurrent systems automatically like model-checkers and symbolically like theorem-provers, in order to support designs of the systems. Then, we have studied on such analysis-tools from two points of views : (1) automatizing proofs in theorem-provers and (2) introducing symbolic computation to model-checkers. In the former (1), we showed that proofs in CSP-Prover, which is a theorem-prover for a concurrency theory called CSP, can be automatized by implementing a model-checking algorithm to CSP-Prover. In the latter (2), we presented a method for automatically analyzing the whole behaviors from structures of concurrent systems and behaviors of component-processes by symbolic computation, and we implemented the analysis-method in a prototype-tool called CONPASU. For example, CONPASU can automatically generate symbolic-labeled transition graphs, which are useful for understanding the behaviors, from concurrent systems with infinite-states.
|
