| Item type |
SIG Technical Reports(1) |
| 公開日 |
2016-02-25 |
| タイトル |
|
|
タイトル |
NetCoreプログラムのCoqによる検証 |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Verification of NetCore Programs by Coq |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
セキュリティ・障害・キャンパスネットワーク |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_18gh |
|
資源タイプ |
technical report |
| 著者所属 |
|
|
|
埼玉大学工学部情報システム工学科 |
| 著者所属 |
|
|
|
埼玉大学工学部情報システム工学科 |
| 著者所属(英) |
|
|
|
en |
|
|
Presently with Departement of Information and Computer Sciences, Saitama University |
| 著者所属(英) |
|
|
|
en |
|
|
Presently with Departement of Information and Computer Sciences, Saitama University |
| 著者名 |
伊達, 弘明
吉浦, 紀晃
|
| 著者名(英) |
Hiroaki, Date
Yoshiura, Noriaki
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
柔軟なパケット転送を行いたいという要求により，OpenFlowが提案されている．OpenFlowスイッチの導入により大規模なネットワーク構築や構成変更をより柔軟に行えるようになった一方，OpenFlowコントローラの転送ルールをプログラミングするため，NetCore，Trema，Freneticなど様々な言語やソフトウェアが開発されてきた．これらのうち，NetCoreとは関数型言語Haskellでプログラミングできる言語であり，宣言型であること，モジュール構造を持っているなどの特徴がある．NetCoreに対する研究として，定理証明支援ソフトCoq上において，そのプログラムの健全性と完全性を証明する事が行われた．この研究により，NetCoreによりプログラミングされた言語が，プログラマの意図した通りにパケットを転送できるかを検証する事が可能となった．本稿では，イッチ同士の接続による閉路が存在するとき，NetCoreによる適切なルール設定により論理的にループを除去することが可能であるかをCoqを用いて検証した． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
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. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AA12326962 |
| 書誌情報 |
研究報告インターネットと運用技術（IOT）
巻 2016-IOT-32,
号 38,
p. 1-8,
発行日 2016-02-25
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
2188-8787 |
| Notice |
|
|
|
SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-IOT16032038.pdf (706.2 kB)
