ソフトウェア設計に対するモデル駆動型検証プロセス(ソフトウェア分析・設計技法)

概要

論文の詳細を見る
本研究では, 新しいソフトウェアプロセスの1つとしてモデル駆動型検証プロセスを提案する.一般に, 設計検証とは, 実践的ノウハウや経験を必要とする, 習得のハードルが非常に高い作業である.しかし, これまで検証プロセスは, それらのノウハウや経験に沿って体系化されていないため, 経験の浅いソフトウェア開発者にとって, 検証は依然として困難な作業となっている.提案プロセスは, この課題に対する解決を目的とするものである.本研究では, 検証プロセスを, 中間成果物である検証モデルに対する変換手続きととらえ, そのうえで検証に必要な具体的作業の順序と内容を体系的に定義する.提案プロセスは次の2つの特長を持つ.第1に, 検証作業に有効な実用的ノウハウの利用方法を明確化している.第2に, 検証モデル間の変換手続きの逆像が, 設計誤り発見のためのデバッグプロセスの定義になっている.さらに, 3つのモデル検査ツール, SPIN, Cadence SMV, LTSAのそれぞれを利用した3つの検証プロセスのインスタンスを示し, 各プロセスをネットワーク家電の制御ソフトウェア設計に適用した事例を示す.その適用結果に基づいて, 提案プロセスの特長と有効性に対する評価について述べる.
2006-01-15