Coqを使ったツリー型ネットワークトポロジ上でのCCNのモデル化と検証について

• Item type: Trans(1)
• 公開日: 2015-09-21
• タイトル: Coqを使ったツリー型ネットワークトポロジ上でのCCNのモデル化と検証について
• タイトル / 言語: en
• タイトル: Formalization and Verification of CCN Protocol on a Tree Topology Using a Proof Assistant Coq
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 関西学院大学理工学研究科情報科学専攻
• 著者所属: 関西学院大学理工学研究科情報科学専攻
• 著者所属: 関西学院大学理工学研究科情報科学専攻
• 著者所属: 関西学院大学理工学研究科情報科学専攻
• 著者所属(英): en
• 著者所属(英): School of Science and Technology, Kwansei Gakuin University
• 著者所属(英): en
• 著者所属(英): School of Science and Technology, Kwansei Gakuin University
• 著者所属(英): en
• 著者所属(英): School of Science and Technology, Kwansei Gakuin University
• 著者所属(英): en
• 著者所属(英): School of Science and Technology, Kwansei Gakuin University
• 著者名: 森嶋, 崇; 後藤, 瑞貴; 森口, 草介; 高橋, 和子
• 著者名(英): Takashi, Morishima; Mizuki, Goto; Sousuke, Moriguchi; Kazuko, Takahashi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Content-Centric Networking（CCN）とは2009年にVan Jacobsenが提案した通信方式であり，アドレスを利用するのではなくコンテンツ名に注目して通信を行うものである．CCNでは中継ノードでコンテンツをキャッシュすることができ，ネットワークの利用効率の向上や，応答時間の短縮が特徴としてあげられる．現在はシミュレーションをベースとして動作や性能のチェックが行われているが，CCNは確立した技術ではないため，実用化にむけて動作の正当性の検証が望まれる．本発表では，証明支援系Coqを用いて，CCNのプロトコルを帰納的にモデル化し，二分木のツリー型ネットワークトポロジにおいて動作の正当性の検証をした．このモデルでは，各ノードで行われているマッチング処理を実装し，1つの時系列リストを用意して，ノード間のパケットの送受信すべてを管理するようにした．動作の正当性として，あるコンテンツがネットワーク上に存在し，ユーザがそれを要求すれば，必ず正しいものを受信できるかということと，その逆の，コンテンツを受信した場合は，そのユーザが要求を送っていたということを証明した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Content-Centric Networking (CCN) is a communication architecture which was developed by Van Jacobsen on 2009. Communication on CCN is based on the names of objects, rather than on addresses. CCN can store contents on relay nodes. It is said that CCN improves network efficiency and reduces response time, but it is not a well-established technique. Although its behavior and performance are explored mainly by simulation, the behavioral correctness is required to be verified for its practical use. In this model, the matching process undertaken on each node is implemented and all events of sending/receiving packets are managed by a unique list. We proved two properties as behavioral correctness of this model on a binary tree topology. First, a user can retrieve the content if it sent the request under the condition that the content exists in the network. Second, a user must have been sent the request for the content if a user receives it under the condition that the content exists in the network. We have implemented the model and proved these properties using a proof assistant Coq.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 8, 号 3, p. 35-35, 発行日 2015-09-21
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会