| 研究課題/領域番号 |
20500023
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 独立行政法人産業技術総合研究所 |
|---|
研究代表者 |
磯部 祥尚 独立行政法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (50356458)
|
|---|
| 研究期間 (年度) |
2008 – 2010
|
| 研究課題ステータス |
完了 (2010年度)
|
| 配分額 *注記 |
3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2010年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2009年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2008年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 並行システム / プロセス代数 / 自動解析ツール / 記号処理 / 状態数削減 / 無限状態システム / 定理証明器 / モデル検査器 / 値渡しプロセス代数 / 解析 / モデル検査 / 検証 |
|---|
| 研究概要 |
本研究では、並行システムの設計を支援するため、モデル検査器のように自動的に、かつ定理証明器のように記号的にそのシステムの動作を解析するツールの開発を目標として、(1)定理証明器の証明自動化と(2)モデル検査器の記号処理化の二つの側面から研究を行った。前者の(1)については、並行動作の理論CSPに基づく定理証明器CSP-Proverにモデル検査の自動検査アルゴリズムを実装し、証明自動化の可能性を示した。後者の(2)については、並行システムの構造や各プロセスの動作から、そのシステム全体の動作を記号処理によって自動解析する方法を提案し、その方法を解析ツールCONPASUとして実装した。例えばCONPASUは、無限状態の並行システムから、その動作を理解するために有益な記号ラベル付き状態遷移図を自動生成することができる。
|
