反例を利用した網羅性の高いプロパティ集合生成手法(高位検証,デザインガイア2008-VLSI設計の新しい大地)

スポンサーリンク

概要

論文の詳細を見る
ソフトウェアとハードウェアが協調動作する大規模なシステムの仕様設計段階における検証は、以降の設計において誤りが生じることを防ぐために非常に重要であるが、仕様記述の不明確さなどのために、検証するプロパティを常に正しく記述することは難しい。本研究では、検証を考慮したシステムの仕様設計段階における設計フローを示すとともに、その設計や後工程の設計を検証するためのプロパティ集合の導出について述べる。一般的に、プロパティを用いた検証では、プロパティの網羅性によって検証の質が決定されるため、プロパティの網羅性の指標、および、より網羅的なプロパティを生成するための工夫・手法が不可欠である。本研究では、有限状態機械として記述された仕様に対して、プロパティの検証時にたどられる状態遷移の割合による網羅性の指標を提案する。また、提案する設計フローにおいて、シミュレーション等を通して、正しくないと判断される実行例からプロパティを生成する手法をエレベータ制御の例題を通して示す。
2008-11-10

著者

関連論文

もっと見る

スポンサーリンク