| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2014-04-25 16:45 証明支援系Coqを使ったCCNのモデル化と検証について ○森嶋 崇・後藤瑞貴・高橋和子（関西学院大）  CPSY2014-8 DC2014-8 |
|
| 抄録 | （和） | Content-Centric Networking(CCN)は2009年に提案された通信方式であり， アドレスではなくコンテンツ名に注目して通信を行うものである． 現在はシミュレーションをベースとして動作や性能のチェックが 行われているが，確立した技術ではないため，実用化にむけて， 動作の正当性の検証が望まれる．本研究では， 証明支援系Coqを用いてCCNのプロトコルを帰納的にモデル化し， 各ノードで行われているマッチング処理を実装した． そのモデル上で，あるコンテンツがネットワーク上に存在するとき， ユーザがそれを要求すれば，必ず正しいものを受信できることを検証した． |
| （英） | Content-Centric Networking (CCN) is a communication architecture which was developed on 2009. Communication on CCN is based on the names of objects, rather than on addresses. Although its behavior and performance are explored mainly by simulation, they have not been well-established, and behavioral correctness is required to be verified for its practicel use. In this paper. we create an inductive model for a CCN protocol and implement the maching process undertaken in each node. Then we prove that a node can retrieve the content if and only if the user sends a request when it exists in the network, as one of behavioral correctness. |
|
| キーワード | （和） | Coq / CCN / behavioral correctness / network protocol / theorem prover / proof assistant / / |
| （英） | Coq / CCN / behavioral correctness / network protocol / theorem prover / proof assistant / / | |
| 文献情報 | 信学技報, vol. 114, no. 22, DC2014-8, pp. 37-42, 2014年4月. | |
| 資料番号 | DC2014-8 | |
| 発行日 | 2014-04-18 (CPSY, DC) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | CPSY2014-8 DC2014-8 |
|
| 研究会情報 | |
| 研究会 | CPSY DC |
| 開催期間 | 2014-04-25 - 2014-04-25 |
| 開催地（和） | 国立情報学研究所 |
| 開催地（英） | |
| テーマ（和） | ディペンダブルコンピューティングシステムおよび一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | DC |
| 会議コード | 2014-04-CPSY-DC |
| 本文の言語 | 日本語 |
| タイトル（和） | 証明支援系Coqを使ったCCNのモデル化と検証について |
| サブタイトル（和） | |
| タイトル（英） | Modeling and verification for CCN using a proof assistant Coq |
| サブタイトル（英） | |
| キーワード(1)（和/英） | Coq / Coq |
| キーワード(2)（和/英） | CCN / CCN |
| キーワード(3)（和/英） | behavioral correctness / behavioral correctness |
| キーワード(4)（和/英） | network protocol / network protocol |
| キーワード(5)（和/英） | theorem prover / theorem prover |
| キーワード(6)（和/英） | proof assistant / proof assistant |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 森嶋 崇 / Takashi Morishima / モリシマ タカシ |
| 第1著者 所属（和/英） | 関西学院大学 (略称： 関西学院大) Kwansei Gakuin University (略称： Kwansei Gakuin Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 後藤 瑞貴 / Mizuki Goto / ゴトウ ミズキ |
| 第2著者 所属（和/英） | 関西学院大学 (略称： 関西学院大) Kwansei Gakuin University (略称： Kwansei Gakuin Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 高橋 和子 / Kazuko Takahashi / タカハシ カズコ |
| 第3著者 所属（和/英） | 関西学院大学 (略称： 関西学院大) Kwansei Gakuin University (略称： Kwansei Gakuin Univ.) |
| 第4著者 氏名（和/英/ヨミ） | / / |
| 第4著者 所属（和/英） | (略称： ) (略称： ) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2014-04-25 16:45:00 |
| 発表時間 | 25分 |
| 申込先研究会 | DC |
| 資料番号 | CPSY2014-8, DC2014-8 |
| 巻番号（vol） | vol.114 |
| 号番号（no） | no.21(CPSY), no.22(DC) |
| ページ範囲 | pp.37-42 |
| ページ数 | 6 |
| 発行日 | 2014-04-18 (CPSY, DC) |
[研究会発表申込システムのトップページに戻る]