| 講演名 | 2008-11-18 反例を利用した網羅性の高いプロパティ集合生成手法(高位検証,デザインガイア2008-VLSI設計の新しい大地) 松本 剛史, 李 蓮福, 吉田 浩章, 余宮 尚志, 藤田 昌宏, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | ソフトウェアとハードウェアが協調動作する大規模なシステムの仕様設計段階における検証は、以降の設計において誤りが生じることを防ぐために非常に重要であるが、仕様記述の不明確さなどのために、検証するプロパティを常に正しく記述することは難しい。本研究では、検証を考慮したシステムの仕様設計段階における設計フローを示すとともに、その設計や後工程の設計を検証するためのプロパティ集合の導出について述べる。一般的に、プロパティを用いた検証では、プロパティの網羅性によって検証の質が決定されるため、プロパティの網羅性の指標、および、より網羅的なプロパティを生成するための工夫・手法が不可欠である。本研究では、有限状態機械として記述された仕様に対して、プロパティの検証時にたどられる状態遷移の割合による網羅性の指標を提案する。また、提案する設計フローにおいて、シミュレーション等を通して、正しくないと判断される実行例からプロパティを生成する手法をエレベータ制御の例題を通して示す。 |
| 抄録(英) | 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. |
| キーワード(和) | 仕様 / 上位設計 / 形式的検証 / プロパティ検証 / UML |
| キーワード(英) | Specification / High-level design / Formal verification / Property checking / UML |
| 資料番号 | VLD2008-79,DC2008-47 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2008/11/10(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 反例を利用した網羅性の高いプロパティ集合生成手法(高位検証,デザインガイア2008-VLSI設計の新しい大地) |
| サブタイトル（和） | |
| タイトル（英） | Generation of High Coverage Property Set Using Counterexamples |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 仕様 / Specification |
| キーワード(2)（和/英） | 上位設計 / High-level design |
| キーワード(3)（和/英） | 形式的検証 / Formal verification |
| キーワード(4)（和/英） | プロパティ検証 / Property checking |
| キーワード(5)（和/英） | UML / UML |
| 第 1 著者 氏名（和/英） | 松本 剛史 / Takeshi MATSUMOTO |
| 第 1 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター VLSI Design and Education Center, University of Tokyo |
| 第 2 著者 氏名（和/英） | 李 蓮福 / Yeonbok LEE |
| 第 2 著者 所属（和/英） | 東京大学大学院工学系研究科電気系工学専攻 Dept. of Electrical Engineering and Information Systems, University of Tokyo |
| 第 3 著者 氏名（和/英） | 吉田 浩章 / Hiroaki YOSHIDA |
| 第 3 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター VLSI Design and Education Center, University of Tokyo |
| 第 4 著者 氏名（和/英） | 余宮 尚志 / Hisashi YOMIYA |
| 第 4 著者 所属（和/英） | 株式会社東芝ソフトウェア技術センター Corporate Software Engineering Center, Toshiba Corporation |
| 第 5 著者 氏名（和/英） | 藤田 昌宏 / Masahiro FUJITA |
| 第 5 著者 所属（和/英） | 東京大学大規模集積システム設計教育研究センター VLSI Design and Education Center, University of Tokyo |
| 発表年月日 | 2008-11-18 |
| 資料番号 | VLD2008-79,DC2008-47 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | 298 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |