2012 Fiscal Year Research-status Report
| Project/Area Number |
24500009
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
西崎 真也 東京工業大学, 情報理工学(系)研究科, 准教授 (90263615)
|
|---|
| Project Period (FY) |
2012-04-01 – 2017-03-31
|
| Keywords | 計算モデル / システム故障 |
|---|
| Research Abstract |
平成２４年度においては、故障をとらえた計算モデルの確立に取り組む。計算モデルの基盤になるものとしてpi計算やACP(Algebra of Communicating Processes)のようなプロセス代数と多くのモデル検査システムで用いられている有限状態オートマトンの２つの枠組みを取り上げた。まず、FMEA(故障モードとその影響の解析）等の故障に関する研究を参考に、故障というものの分類を行い、プロセス代数ベース計算モデル、および、有限状態オートマトンベース計算モデルの枠組みにおいて故障の定式化を行う。各々のモデルにおいても意味論をあたえ、その性質について研究していった。また、プロセス代数ベースモデルにおいては、簡約を行うソフトウェアツールのプロトタイプ実装と、有限状態オートマトンベースモデルにおいてはモデル間変換のプロトタイプ実装の準備と検討を行った。
また、システム故障時（ハードウェア故障、ネットワーク不調等）における、ソフトウェアシステムの挙動を解析するためのソフトウェア検証技術・形式的開発手法の確立を研究目的とする。故障という現象をとらえた計算モデルを確立し、その計算モデルに基づき、モデル検査を応用することにより、故障時におけるシステムの挙動解析を目指した。そのために以下のような事項に取り組んでいった
①システム故障の計算モデルを与える。
②その計算モデルから従来の計算モデルへの変換に基づく故障時の振る舞いの解析手法を提案する。
③その解析手法を支援する検証システムを開発する。
④計算モデルの定理証明システム上での形式化に取り組む。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
計画にしたがって研究を遂行し、予定通りの成果を得ることができた。
研究発表の機会を通して、国内外の研究者との交流の機会を増やすことにより、有益なコメントをえることを通して、研究の進展において、良い研究方向・研究遂行方法を捉えることが可能となり、効率的・効果的な研究を進めることができた。
|
| Strategy for Future Research Activity |
平成２５年度以降においても、研究の目的として、システム故障時（ハードウェア故障、ネットワーク不調等）における、ソフトウェアシステムの挙動を解析するためのソフトウェア検証技術・形式的開発手法の確立を研究目的とする。故障という現象をとらえた計算モデルを確立し、その計算モデルに基づき、モデル検査を応用することにより、故障時におけるシステムの挙動解析を目指す。そのために以下のような事項に取り組んでゆく。
①システム故障の計算モデルを与える。
②その計算モデルから従来の計算モデルへの変換に基づく故障時の振る舞いの解析手法を提案する。
③その解析手法を支援する検証システムを開発する。
④計算モデルの定理証明システム上での形式化に取り組む。
|
| Expenditure Plans for the Next FY Research Funding |
該当なし
|
