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

森嶋 崇; 後藤 瑞貴; 森口 草介; 高橋 和子

論文・著書情報

タイトル

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

著者

和文:	森嶋崇, 後藤瑞貴, 森口草介, 高橋和子.
英文:	森嶋崇, 後藤瑞貴, Sosuke Moriguchi, 高橋和子.

言語

Japanese

掲載誌/書名

和文:	情報処理学会論文誌プログラミング（PRO）
英文:

巻, 号, ページ

Vol. 8 No. 3 pp. 35-35

出版年月

2015年8月

出版者

和文:
英文:

会議名称

和文:
英文:

開催地

和文:
英文:

アブストラクト

Content-Centric Networking（CCN）とは2009年にVan Jacobsenが提案した通信方式であり，アドレスを利用するのではなくコンテンツ名に注目して通信を行うものである．CCNでは中継ノードでコンテンツをキャッシュすることができ，ネットワークの利用効率の向上や，応答時間の短縮が特徴としてあげられる．現在はシミュレーションをベースとして動作や性能のチェックが行われているが，CCNは確立した技術ではないため，実用化にむけて動作の正当性の検証が望まれる．本発表では，証明支援系Coqを用いて，CCNのプロトコルを帰納的にモデル化し，二分木のツリー型ネットワークトポロジにおいて動作の正当性の検証をした．このモデルでは，各ノードで行われているマッチング処理を実装し，1つの時系列リストを用意して，ノード間のパケットの送受信すべてを管理するようにした．動作の正当性として，あるコンテンツがネットワーク上に存在し，ユーザがそれを要求すれば，必ず正しいものを受信できるかということと，その逆の，コンテンツを受信した場合は，そのユーザが要求を送っていたということを証明した．

Home

各種検索

サポート

T2R2について

関連リンク

論文・著書情報