| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2009-01-30 09:05 仕様から自動生成されたプロパティによるプロトコル変換機の形式的検証手法 ○高 飛・西原 佑・松本剛史・藤田昌宏（東大）  VLD2008-110 CPSY2008-72 RECONF2008-74 |
|
| 抄録 | （和） | 近年、設計期間を短縮するために設計資産の再利用がよく行われている。その際、異なるインタフェースを持つ設計同士を接続する場合にはプロトコル変換器を設計し挿入する必要がある。そのため、設計資産再利用を行う設計において、プロトコル変換器の設計と検証は重要である。そこで、本研究では、異なるプロトコルで通信するモジュール間を接続するプロトコル変換器の形式的検証手法を提案する。提案手法では、通信する双方のプロトコルの仕様の積を取ることにより、プロトコル変換器設計の仕様を得る。その後、シミュレーションによって、その仕様のうち設計において実装されている部分を抽出し、そこから設計が満たすべきプロパティを作成する。最終的に、このプロパティによって形式的検証を行い、全てのプロパティを満たせば設計の正しさを証明することができる。実験として、提案手法によるAMBA とOCP のプロトコル変換器に対する検証結果を示す。 |
| （英） | IP-reuse design is widely applied in order to reduce design period by utilizing already designed and well verified modules. When two IPs have different interfaces, it is necessary to design a protocol transducer to transduce the different protocols between them. In this paper, we propose a method to formally verify protocol transducers which transduce the different protocols. In our method, firstly, we generate the specification of the transducer under verification from the specification of the protocols. Next, a subset of the specification which is implemented in the transducer design is extracted by random simulation. Then, a set of properties that should be satisfied in the design is generated. If all of those properties are satisfied, the correctness of the protocol transducer design is proved. We also show the results of the experiments for transducer designs connecting AMBA and OCP protocols. | |
| キーワード | （和） | プロトコル変換器 / 形式的検証 / プロパティ検証 / 仕様 / / / / |
| （英） | Protocol transcuder / Formal verification / Property checking / Specification / / / / | |
| 文献情報 | 信学技報, vol. 108, no. 412, VLD2008-110, pp. 111-116, 2009年1月. | |
| 資料番号 | VLD2008-110 | |
| 発行日 | 2009-01-22 (VLD, CPSY, RECONF) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | VLD2008-110 CPSY2008-72 RECONF2008-74 |
|
| 研究会情報 | |
| 研究会 | VLD CPSY RECONF IPSJ-SLDM |
| 開催期間 | 2009-01-29 - 2009-01-30 |
| 開催地（和） | 慶応義塾大学(日吉) |
| 開催地（英） | |
| テーマ（和） | FPGA応用および一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | VLD |
| 会議コード | 2009-01-VLD-CPSY-RECONF-SLDM |
| 本文の言語 | 日本語 |
| タイトル（和） | 仕様から自動生成されたプロパティによるプロトコル変換機の形式的検証手法 |
| サブタイトル（和） | |
| タイトル（英） | Formal Verification Method for Protocol Transducer Using Automatically Generated Properties from Specification |
| サブタイトル（英） | |
| キーワード(1)（和/英） | プロトコル変換器 / Protocol transcuder |
| キーワード(2)（和/英） | 形式的検証 / Formal verification |
| キーワード(3)（和/英） | プロパティ検証 / Property checking |
| キーワード(4)（和/英） | 仕様 / Specification |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 高 飛 / Fei Gao / コー ヒ |
| 第1著者 所属（和/英） | 東京大学 (略称： 東大) University of Tokyo (略称： Univ. of Tokyo) |
| 第2著者 氏名（和/英/ヨミ） | 西原 佑 / Tasuku Nishihara / ニシハラ タスク |
| 第2著者 所属（和/英） | 東京大学 (略称： 東大) University of Tokyo (略称： Univ. of Tokyo) |
| 第3著者 氏名（和/英/ヨミ） | 松本 剛史 / Takeshi Matsumoto / マツモト タケシ |
| 第3著者 所属（和/英） | 東京大学 (略称： 東大) University of Tokyo (略称： Univ. of Tokyo) |
| 第4著者 氏名（和/英/ヨミ） | 藤田 昌宏 / Masahiro Fujita / フジタ マサヒロ |
| 第4著者 所属（和/英） | 東京大学 (略称： 東大) University of Tokyo (略称： Univ. of Tokyo) |
| 講演者 | 第1著者 |
| 発表日時 | 2009-01-30 09:05:00 |
| 発表時間 | 25分 |
| 申込先研究会 | VLD |
| 資料番号 | VLD2008-110, CPSY2008-72, RECONF2008-74 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | no.412(VLD), no.413(CPSY), no.414(RECONF) |
| ページ範囲 | pp.111-116 |
| ページ数 | 6 |
| 発行日 | 2009-01-22 (VLD, CPSY, RECONF) |
[研究会発表申込システムのトップページに戻る]