| 研究課題/領域番号 |
24500009
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
西崎 真也 東京工業大学, 情報理工学(系)研究科, 准教授 (90263615)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2017-03-31
|
| キーワード | 計算モデル / システム故障 |
|---|
| 研究概要 |
平成２４年度においては、故障をとらえた計算モデルの確立に取り組む。計算モデルの基盤になるものとしてpi計算やACP(Algebra of Communicating Processes)のようなプロセス代数と多くのモデル検査システムで用いられている有限状態オートマトンの２つの枠組みを取り上げた。まず、FMEA(故障モードとその影響の解析）等の故障に関する研究を参考に、故障というものの分類を行い、プロセス代数ベース計算モデル、および、有限状態オートマトンベース計算モデルの枠組みにおいて故障の定式化を行う。各々のモデルにおいても意味論をあたえ、その性質について研究していった。また、プロセス代数ベースモデルにおいては、簡約を行うソフトウェアツールのプロトタイプ実装と、有限状態オートマトンベースモデルにおいてはモデル間変換のプロトタイプ実装の準備と検討を行った。
また、システム故障時（ハードウェア故障、ネットワーク不調等）における、ソフトウェアシステムの挙動を解析するためのソフトウェア検証技術・形式的開発手法の確立を研究目的とする。故障という現象をとらえた計算モデルを確立し、その計算モデルに基づき、モデル検査を応用することにより、故障時におけるシステムの挙動解析を目指した。そのために以下のような事項に取り組んでいった
①システム故障の計算モデルを与える。
②その計算モデルから従来の計算モデルへの変換に基づく故障時の振る舞いの解析手法を提案する。
③その解析手法を支援する検証システムを開発する。
④計算モデルの定理証明システム上での形式化に取り組む。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
計画にしたがって研究を遂行し、予定通りの成果を得ることができた。
研究発表の機会を通して、国内外の研究者との交流の機会を増やすことにより、有益なコメントをえることを通して、研究の進展において、良い研究方向・研究遂行方法を捉えることが可能となり、効率的・効果的な研究を進めることができた。
|
| 今後の研究の推進方策 |
平成２５年度以降においても、研究の目的として、システム故障時（ハードウェア故障、ネットワーク不調等）における、ソフトウェアシステムの挙動を解析するためのソフトウェア検証技術・形式的開発手法の確立を研究目的とする。故障という現象をとらえた計算モデルを確立し、その計算モデルに基づき、モデル検査を応用することにより、故障時におけるシステムの挙動解析を目指す。そのために以下のような事項に取り組んでゆく。
①システム故障の計算モデルを与える。
②その計算モデルから従来の計算モデルへの変換に基づく故障時の振る舞いの解析手法を提案する。
③その解析手法を支援する検証システムを開発する。
④計算モデルの定理証明システム上での形式化に取り組む。
|
| 次年度の研究費の使用計画 |
該当なし
|
