反例と設計分割に基づく高位設計に対する効率的な設計修正支援手法(検証技術,システム設計及び一般)

スポンサーリンク

概要

論文の詳細を見る
高位設計記述において、シミュレーションや形式的手法によって機能仕様に反する実行例(反例)が発見された場合、その反例や機能仕様を参照しながら、設計記述をデバッグする必要がある。本稿では、このように反例に基づくデバッグ作業を支援する手法を提案する。具体的には、与えられた反例および正しい実行例から、全てのテストパタンを正しく実行するための設計記述修正の候補を形式的に求める。これにより、設計者は、修正すべき箇所と修正方法の候補を得ることができ、より効率的にデバッグ作業を行えることが期待できる。提案手法では、反例入力パタンによって正しい実行結果を得るためには、どの変数値を実行値とは異なる値に置換すれば良いか、をSMTソルバーを用いて解いている。加えて、効率的に修正候補を求めるために、設計を分割し、部分的にこれを適用する手法を提案する。実験により、提案手法によって、設計中の設計誤りを正す修正を求めることがでることを示す。
2011-05-11

著者

関連論文

もっと見る

スポンサーリンク