{"updated":"2025-01-20T13:15:38.859391+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00157723","sets":["1164:4088:8487:8488"]},"path":["8488"],"owner":"11","recid":"157723","title":["NetCoreプログラムのCoqによる検証"],"pubdate":{"attribute_name":"公開日","attribute_value":"2016-02-25"},"_buckets":{"deposit":"f29322b9-9de7-4fbf-b9eb-fb7deec2522d"},"_deposit":{"id":"157723","pid":{"type":"depid","value":"157723","revision_id":0},"owners":[11],"status":"published","created_by":11},"item_title":"NetCoreプログラムのCoqによる検証","author_link":["299023","299024","299026","299025"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"NetCoreプログラムのCoqによる検証"},{"subitem_title":"Verification of NetCore Programs by Coq","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"セキュリティ・障害・キャンパスネットワーク","subitem_subject_scheme":"Other"}]},"item_type_id":"4","publish_date":"2016-02-25","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"埼玉大学工学部情報システム工学科"},{"subitem_text_value":"埼玉大学工学部情報システム工学科"}]},"item_4_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Presently with Departement of Information and Computer Sciences, Saitama University","subitem_text_language":"en"},{"subitem_text_value":"Presently with Departement of Information and Computer Sciences, Saitama 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/157723/files/IPSJ-IOT16032038.pdf","label":"IPSJ-IOT16032038.pdf"},"date":[{"dateType":"Available","dateValue":"2018-02-25"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-IOT16032038.pdf","filesize":[{"value":"706.2 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"43"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"7a5eb517-ef8f-4bef-87bc-a9ce8f02ea09","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2016 by the Information Processing Society of Japan"}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"伊達, 弘明"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"吉浦, 紀晃"}],"nameIdentifiers":[{}]}]},"item_4_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Hiroaki, Date","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yoshiura, Noriaki","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_4_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA12326962","subitem_source_identifier_type":"NCID"}]},"item_4_textarea_12":{"attribute_name":"Notice","attribute_value_mlt":[{"subitem_textarea_value":"SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc."}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_18gh","resourcetype":"technical report"}]},"item_4_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"2188-8787","subitem_source_identifier_type":"ISSN"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"柔軟なパケット転送を行いたいという要求により，OpenFlowが提案されている．OpenFlowスイッチの導入により大規模なネットワーク構築や構成変更をより柔軟に行えるようになった一方，OpenFlowコントローラの転送ルールをプログラミングするため，NetCore，Trema，Freneticなど様々な言語やソフトウェアが開発されてきた．これらのうち，NetCoreとは関数型言語Haskellでプログラミングできる言語であり，宣言型であること，モジュール構造を持っているなどの特徴がある．NetCoreに対する研究として，定理証明支援ソフトCoq上において，そのプログラムの健全性と完全性を証明する事が行われた．この研究により，NetCoreによりプログラミングされた言語が，プログラマの意図した通りにパケットを転送できるかを検証する事が可能となった．本稿では，イッチ同士の接続による閉路が存在するとき，NetCoreによる適切なルール設定により論理的にループを除去することが可能であるかをCoqを用いて検証した．","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"OpenFlow is proposed for flexible forwarding of packets. OpenFlow enables to construct and change large networks flexibly. Several programming languages such NetCore, Trema and Frenetic have been proposed for configurations of OpenFlow controllers. NetCore can be used in Haskell, which is a functional programming language. There are several features of NetCore. NetCore is a declarative programming language and has a module structure. Programming in NetCore can be verified on Coq, which is a formal proof management system. This paper uses Coq to verify NetCore programmings for networks that consist of several OpenFlow Switches. Especially, this paper focus on verification of loop-free networks.","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"8","bibliographic_titles":[{"bibliographic_title":"研究報告インターネットと運用技術（IOT）"}],"bibliographicPageStart":"1","bibliographicIssueDates":{"bibliographicIssueDate":"2016-02-25","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"38","bibliographicVolumeNumber":"2016-IOT-32"}]},"relation_version_is_last":true,"weko_creator_id":"11"},"created":"2025-01-19T00:31:35.952433+00:00","id":157723,"links":{}}