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
|
| Project Status |
Completed (Fiscal Year 2010)
|
| Budget Amount *help |
¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2010: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2009: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2008: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| 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.
|
Report
(4 results)
Research Products
(47 results)
