システム故障時(ハードウェア故障、ネットワーク不調等)における、ソフトウェアシステムの挙動を解析するためのソフトウェア検証技術・形式的開発手法の確立を研究目的とした。故障という現象をとらえた計算モデルを研究し、その計算モデルに基づき、モデル検査を応用することにより、故障時におけるシステムの挙動解析を研究し以下のような事項に取り組んだ。 ①システム故障の計算モデル②その計算モデルから従来の計算モデルへの変換に基づく故障時の振る舞いの解析手法の提案③その解析手法を支援する検証システムの開発④計算モデルの定理証明システム上での形式化
|