| 講演名 | 2005-10-21 モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法(プロセッサ, DSP, 画像処理技術及び一般) 垣内 洋介, 北嶋 暁, 浜口 清治, 柏原 敏伸, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本論文では, ハードウェアインターフェース仕様全体をより包括的に検証することを目指し, 正規表現ベースの仕様記述言語からモニタ回路を生成する手法を示す.モニタ回路の生成は自動的に行われるため, 複雑な仕様に対するモニタ回路であっても人手で設計する場合に比べ, 誤りの混入を避けることができる.また, モジュール単位の検証の際, 通常では入力制約を付加する必要があるが, 本論文では仕様記述から, 入力制約を自動的に抽出して, モニタ回路に直接反映させる手法について述べる.実験では設計例としてバスプロトコルであるAMBA AHBに従って設計された回路を取り上げ, 実際に仕様を記述してモニタを生成し, 形式検証を行った結果を示す. |
| 抄録(英) | In order to verify hardware module interfaces, various verification methods have been proposed. This paper focuses on formal monitor-based verification of module interfaces. In our method, first, we describe specifications of module interfaces in a language based on regular expressions, then construct behavior models from the description. Finally, we generate a monitor circuit. When we verify module interfaces formally, some input constraints are usually required. We show how to generate monitors including input constraints automatically from specifications. In verification experiments, we show that modules that comply AMBA AHB bus protocol can be verified by monitors formally. |
| キーワード(和) | 形式検証 / モニタベース検証 / モニタ回路生成 |
| キーワード(英) | Formal Verification / Monitor-based Verification / AMBA / Monitor Circuit Generation |
| 資料番号 | SIP2005-127,ICD2005-146,IE2005-91 |
| 発行日 |
| 研究会情報 | |
| 研究会 | ICD |
|---|---|
| 開催期間 | 2005/10/14(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Integrated Circuits and Devices (ICD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法(プロセッサ, DSP, 画像処理技術及び一般) |
| サブタイトル（和） | |
| タイトル（英） | A Monitor Generation Method for Formal Monitor-based Verification Considering Input Constraints |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式検証 / Formal Verification |
| キーワード(2)（和/英） | モニタベース検証 / Monitor-based Verification |
| キーワード(3)（和/英） | モニタ回路生成 / AMBA |
| 第 1 著者 氏名（和/英） | 垣内 洋介 / Yosuke KAKIUCHI |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 北嶋 暁 / Akira KITAJIMA |
| 第 2 著者 所属（和/英） | 大阪電気通信大学総合情報学部メディアコンピュータシステム学科 Faculty of Information Science and Technology, Osaka Electro-Communication University |
| 第 3 著者 氏名（和/英） | 浜口 清治 / Kiyoharu HAMAGUCHI |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 4 著者 氏名（和/英） | 柏原 敏伸 / Toshinobu KASHIWABARA |
| 第 4 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2005-10-21 |
| 資料番号 | SIP2005-127,ICD2005-146,IE2005-91 |
| 巻番号（vol） | vol.105 |
| 号番号（no） | 352 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |