反例を利用した網羅性の高いプロパティ集合生成手法

摘要

When we design a large system including hardware and software, verification in specification-level is very important to avoid design bugs from the subsequent design-levels such as system-level and behavior-level. However, partly because the specification documents itself has unclarity and ambiguity, correctly writing properties to be kept in designs is difficult. In this work, we propose a high-level design flow considering verification and property derivation in that flow. In general, the quality of property checking is decided by the completeness of a set of given properties. Therefore, metrics to measure the completeness of the property set and methods to generate properties with high completeness are required. We propose a transition-based coverage metric that is defined in finite state machine of the system specification. Through a case study of an elevator controller design, we also show a way to generate properties that can improve the coverage from counterexamples found in simulation.%ソフトウェアとハードウェアが協調動作する大規模なシステムの仕様設計段階における検証は、以降の設計において誤りが生じることを防ぐために非常に重要であるが、仕様記述の不明確さなどのために、検証するプロパティを常に正しく記述することは難しい。本研究では、検証を考慮したシステムの仕様設計段階における設計フローを示すとともに、その設計や後工程の設計を検証するためのプロパティ集合の導出について述べる。一般的に、プロパティを用いた検証では、プロパティの網羅性によって検証の質が決定されるため、プロパティの網羅性の指標、および、より網羅的なプロパティを生成するための工夫・手法が不可欠である。本研究では、有限状態機械として記述された仕様に対して、プロパティの検証時にたどられる状態遷移の割合による網羅性の指標を提案する。また、提案する設計フローにおいて、シミュレーション等を通して、正しくないと判断される実行例からプロパティを生成する手法をエレベータ制御の例題を通して示す。