2010 Fiscal Year Annual Research Report
| Project/Area Number |
20500023
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
磯部 祥尚 独立行政法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (50356458)
|
|---|
| Keywords | 並行システム / 値渡しプロセス代数 / 自動解析ツール / 記号処理 / 状態数削減 / 無限状態システム |
|---|
| Research Abstract |
本研究では、記号処理による並行システム解析支援ツールCONPASUを開発した。CONPASUは、変数を値で具体化せずに記号処理によって並行動作を自動的に解析することができ、モデル検査器(自動検査)と定理証明器(記号処理)の両方の特徴をもつツールである。記号処理は無限状態システムも扱えるなどの利点があるが、一般にはその動作を完全に自動解析することはできない。平成22年度は、並行システムの動作を自動解析するために有効な状態数削減法を考案し、その手法をCONPASUに実装した。以下、その成果を平成22年度の前半と後半に分けて説明する。
[平成22年度前半]
弱双模倣等価性と呼ばれる振舞いの等しさを保存するように、観測できない内部動作をバイパスする状態数削減法を考案し、その手法をCONPASUのプロトタイプに実装してその有効性を示した(例:変数を具体化すると変域[0,24]で状態数10,944になる動作を、CONPASUでは無限の変域でも状態数8で表現可能)。また、CONPASUでは確認したい一部の動作に着目した部分仕様を自動生成できるなど、既存ツールにはない結果を得ることもできた。その成果を査読付きワークショップ(FOSE2010)で発表した。
[平成22年度後半]
前半(FOSE2010)の成果によって記号処理による解析の有効性を示すことができたが、弱双模倣等価性では条件付の内部動作を適切にバイパスすることができなかった。そこで、弱双模倣等価性の代わりに失敗等価性を採用することによってその問題を解決した。また、一度得られたバイパス可能な遷移の探索結果を、繰り返し再利用して状態数を削減できるようにしたことも本手法で工夫した点の一つである。この失敗等価性を保存する状態数削減法をCONPASUに実装し(Java言語,6,000行程度)、その有効性を示した。その成果を論文にまとめて国際会議(CPA2011)に投稿し、採択された(2011年6月発表予定)。
|
