{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00145142","sets":["934:935:8226:8284"]},"path":["8284"],"owner":"11","recid":"145142","title":["Coqを使ったツリー型ネットワークトポロジ上でのCCNのモデル化と検証について"],"pubdate":{"attribute_name":"公開日","attribute_value":"2015-09-21"},"_buckets":{"deposit":"1517a09d-4122-4da8-9a1d-67d599d85946"},"_deposit":{"id":"145142","pid":{"type":"depid","value":"145142","revision_id":0},"owners":[11],"status":"published","created_by":11},"item_title":"Coqを使ったツリー型ネットワークトポロジ上でのCCNのモデル化と検証について","author_link":["222372","222373","222371","222377","222375","222370","222374","222376"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Coqを使ったツリー型ネットワークトポロジ上でのCCNのモデル化と検証について"},{"subitem_title":"Formalization and Verification of CCN Protocol on a Tree Topology Using a Proof Assistant Coq","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"[発表概要]","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2015-09-21","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"関西学院大学理工学研究科情報科学専攻"},{"subitem_text_value":"関西学院大学理工学研究科情報科学専攻"},{"subitem_text_value":"関西学院大学理工学研究科情報科学専攻"},{"subitem_text_value":"関西学院大学理工学研究科情報科学専攻"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"School of Science and Technology, Kwansei Gakuin University","subitem_text_language":"en"},{"subitem_text_value":"School of Science and Technology, Kwansei Gakuin University","subitem_text_language":"en"},{"subitem_text_value":"School of Science and Technology, Kwansei Gakuin University","subitem_text_language":"en"},{"subitem_text_value":"School of Science and Technology, Kwansei Gakuin University","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/145142/files/IPSJ-TPRO0803008.pdf","label":"IPSJ-TPRO0803008.pdf"},"date":[{"dateType":"Available","dateValue":"2017-09-21"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO0803008.pdf","filesize":[{"value":"103.2 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"5"},{"tax":["include_tax"],"price":"0","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"3ff4b39c-d462-4002-b7bc-eb46134bbfc9","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2015 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"森嶋, 崇"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"後藤, 瑞貴"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"森口, 草介"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"高橋, 和子"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Takashi, Morishima","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Mizuki, Goto","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Sousuke, Moriguchi","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Kazuko, Takahashi","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"Content-Centric Networking（CCN）とは2009年にVan Jacobsenが提案した通信方式であり，アドレスを利用するのではなくコンテンツ名に注目して通信を行うものである．CCNでは中継ノードでコンテンツをキャッシュすることができ，ネットワークの利用効率の向上や，応答時間の短縮が特徴としてあげられる．現在はシミュレーションをベースとして動作や性能のチェックが行われているが，CCNは確立した技術ではないため，実用化にむけて動作の正当性の検証が望まれる．本発表では，証明支援系Coqを用いて，CCNのプロトコルを帰納的にモデル化し，二分木のツリー型ネットワークトポロジにおいて動作の正当性の検証をした．このモデルでは，各ノードで行われているマッチング処理を実装し，1つの時系列リストを用意して，ノード間のパケットの送受信すべてを管理するようにした．動作の正当性として，あるコンテンツがネットワーク上に存在し，ユーザがそれを要求すれば，必ず正しいものを受信できるかということと，その逆の，コンテンツを受信した場合は，そのユーザが要求を送っていたということを証明した．","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"35","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicPageStart":"35","bibliographicIssueDates":{"bibliographicIssueDate":"2015-09-21","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"3","bibliographicVolumeNumber":"8"}]},"relation_version_is_last":true,"weko_creator_id":"11"},"id":145142,"updated":"2025-01-20T18:28:06.836158+00:00","links":{},"created":"2025-01-19T00:20:49.052088+00:00"}