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

• Item type: SIG Technical Reports(1)
• 公開日: 2008-11-10
• タイトル: 反例を利用した網羅性の高いプロパティ集合生成手法
• タイトル / 言語: en
• タイトル: Generation of High Coverage Property Set Using Counterexamples
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属: 東京大学大学院工学系研究科電気系工学専攻
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属: 株式会社東芝ソフトウェア技術センター
• 著者所属: 東京大学大規模集積システム設計教育研究センター
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, University of Tokyo
• 著者所属(英): en
• 著者所属(英): Dept. of Electrical Engineering and Information Systems, University of Tokyo
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, University of Tokyo
• 著者所属(英): en
• 著者所属(英): Corporate Software Engineering Center, Toshiba Corporation
• 著者所属(英): en
• 著者所属(英): VLSI Design and Education Center, University of Tokyo
• 著者名: 松本, 剛史; 李, 蓮福; 吉田, 浩章; 余宮, 尚志; 藤田, 昌宏
• 著者名(英): Takeshi, Matsumoto; Yeonbok, Lee; Hiroaki, Yoshida; Hisashi, Yomiya; Masahiro, Fujita
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: ソフトウェアとハードウェアが協調動作する大規模なシステムの仕様設計段階における検証は、以降の設計において誤りが生じることを防ぐために非常に重要であるが、仕様記述の不明確さなどのために、検証するプロパティを常に正しく記述することは難しい。本研究では、検証を考慮したシステムの仕様設計段階における設計フローを示すとともに、その設計や後工程の設計を検証するためのプロパティ集合の導出について述べる。一般的に、プロパティを用いた検証では、プロパティの網羅性によって検証の質が決定されるため、プロパティの網羅性の指標、および、より網羅的なプロパティを生成するための工夫・手法が不可欠である。本研究では、有限状態機械として記述された仕様に対して、プロパティの検証時にたどられる状態遷移の割合による網羅性の指標を提案する。また、提案する設計フローにおいて、シミュレーション等を通して、正しくないと判断される実行例からプロパティを生成する手法をエレベータ制御の例題を通して示す。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11451459
• 書誌情報: 情報処理学会研究報告システムLSI設計技術（SLDM）; 巻 2008, 号 111(2008-SLDM-137), p. 115-120, 発行日 2008-11-10
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会