| 講演名 | 1998/5/22 正規表現を利用したスケーラブル環状回路の検証 戸島 弘詩, 米田 友洋, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 一般的なシステムは少種類の構成要素を多数組合せた規則性の高い構造を持つことが知られているが, このようなシステムを検証する際に全体の構造を維持しつつ縮小したシステムを検証することで, 元のシステムを直接検証するのと同程度の効果があることが直感的に知られている.(例えば, 16bit加算器を2bit加算器に縮小して検証する).しかしそのような検証は, 元々のシステムで同様に検証が成功することを保証しない.本研究では, 環状及び鎖状構造を持ったペトリネットで表現できるシステムを対象として, 任意の規模のシステムを検証する事を目的とし, 正規表現を利用した状態空間の探索手法を提案した.なお, この手法により正規表現された仕様を扱う事が可能となった. |
| 抄録(英) | It is known that many systems have regular structure constructed from several kinds of many modules. When we verify such systems, we intuitively expect that verifying reduced systems whitch preserve the original global structure is equivalent to directly verifying the original systems (e.g. in order to verify a 16bit adder, we verify the reduced 2bit adder instead). However, success of such verification does not guarantee the correctness of the original systems. In this paper, we forcus on the systems expressed by Petri nets with ring or cascade structure, and aim at the verification of such systems with arbitrary sizes. For this purpose, we propose algorithms which explore the state space of ring-structure Petri nets without fixing their size by using regular expression. This also allows us to express specification by regular expression. |
| キーワード(和) | 形式的検証 / 正規表現 / 抽象化 / ペトリネット / スケーラブル環状回路 |
| キーワード(英) | fomal verification / regular expression / abstraction / Petri nets / scalable circuits with ring structure |
| 資料番号 | |
| 発行日 |
| 研究会情報 | |
| 研究会 | ICD |
|---|---|
| 開催期間 | 1998/5/22(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Integrated Circuits and Devices (ICD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 正規表現を利用したスケーラブル環状回路の検証 |
| サブタイトル（和） | |
| タイトル（英） | Verification of Scalable Circuits with Ring Structure by Using Regular Expression |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式的検証 / fomal verification |
| キーワード(2)（和/英） | 正規表現 / regular expression |
| キーワード(3)（和/英） | 抽象化 / abstraction |
| キーワード(4)（和/英） | ペトリネット / Petri nets |
| キーワード(5)（和/英） | スケーラブル環状回路 / scalable circuits with ring structure |
| 第 1 著者 氏名（和/英） | 戸島 弘詩 / Hiroshi TOSHIMA |
| 第 1 著者 所属（和/英） | 東京工業大学大学院情報理工学研究科計算工学専攻 Graduate School of Information Science and Engineering, Department of Computer Science Tokyo Institute of Technology |
| 第 2 著者 氏名（和/英） | 米田 友洋 / Tomohiro YONEDA |
| 第 2 著者 所属（和/英） | 東京工業大学大学院情報理工学研究科計算工学専攻 Graduate School of Information Science and Engineering, Department of Computer Science Tokyo Institute of Technology |
| 発表年月日 | 1998/5/22 |
| 資料番号 | |
| 巻番号（vol） | vol.98 |
| 号番号（no） | 66 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |