@article{oai:ipsj.ixsq.nii.ac.jp:00145142,
 author = {森嶋, 崇 and 後藤, 瑞貴 and 森口, 草介 and 高橋, 和子 and Takashi, Morishima and Mizuki, Goto and Sousuke, Moriguchi and Kazuko, Takahashi},
 issue = {3},
 journal = {情報処理学会論文誌プログラミング（PRO）},
 month = {Sep},
 note = {Content-Centric Networking（CCN）とは2009年にVan Jacobsenが提案した通信方式であり，アドレスを利用するのではなくコンテンツ名に注目して通信を行うものである．CCNでは中継ノードでコンテンツをキャッシュすることができ，ネットワークの利用効率の向上や，応答時間の短縮が特徴としてあげられる．現在はシミュレーションをベースとして動作や性能のチェックが行われているが，CCNは確立した技術ではないため，実用化にむけて動作の正当性の検証が望まれる．本発表では，証明支援系Coqを用いて，CCNのプロトコルを帰納的にモデル化し，二分木のツリー型ネットワークトポロジにおいて動作の正当性の検証をした．このモデルでは，各ノードで行われているマッチング処理を実装し，1つの時系列リストを用意して，ノード間のパケットの送受信すべてを管理するようにした．動作の正当性として，あるコンテンツがネットワーク上に存在し，ユーザがそれを要求すれば，必ず正しいものを受信できるかということと，その逆の，コンテンツを受信した場合は，そのユーザが要求を送っていたということを証明した．, 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.},
 pages = {35--35},
 title = {Coqを使ったツリー型ネットワークトポロジ上でのCCNのモデル化と検証について},
 volume = {8},
 year = {2015}
}