| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2013-07-19 15:15 記号実行によるパケットの抽象化を用いたOpenFlowネットワークのモデル検査方式の提案 ○八鍬 豊・富沢伸行・登内敏夫（NEC）  IN2013-54 |
|
| 抄録 | （和） | OpenFlowネットワークに対し，モデル検査を用いて転送ループ等の不具合の有無を検証する方式を提案する．モデル検査では，各ノードが実行し得る状態を，パケットの到着順が入れ替わる場合も含め網羅的に探索できる．一方，検証対象の規模が大きくなると，モデル検査に要する計算量が指数的に増大してしまう．そこで，モデル検査に記号実行を組み合わせ，計算量を低減する方式を提案する．本方式では，ネットワークの状態探索を行う際，パケットの内容を記号的に表現し遷移を実行する．さらに，各ノードが実行する動作の実行条件を制約として管理し制約ソルバに与えることで，その動作が実際に起こり得るか否かを判断，不要な探索を避ける．これにより，OpenFlowネットワークの効率的な検証が可能になる． |
| （英） | We propose a verification method of the OpenFlow network with the model checking, which can detect a loop routing and so on by emulating all interleaving sequences of packets in the network. The model checking is powerful, but the calculation time increases exponentially when the network is getting large. In order to reduce the calculation time, we use a symbolic execution approach: the contents of packets are expressed as symbols. The proposed method emulates the behavior of nodes in the network, by referring the packets expressed in symbols, and generates symbolic-expressed constraints under which each emulation step must satisfy. By using a constraint solver, the proposed method can skip the emulation steps whose symbolic-expressed constraints cannot be satisfied. So, the proposed method can efficiently verify the OpenFlow network. | |
| キーワード | （和） | Software-Defined Networking / OpenFlow / 記号実行 / 形式手法 / モデル検査 / / / |
| （英） | Software-Defined Networking / OpenFlow / Symbolic execution / Formal methods / Model checking / / / | |
| 文献情報 | 信学技報, vol. 113, no. 140, IN2013-54, pp. 107-112, 2013年7月. | |
| 資料番号 | IN2013-54 | |
| 発行日 | 2013-07-11 (IN) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | IN2013-54 |
|
| 研究会情報 | |
| 研究会 | IN NV |
| 開催期間 | 2013-07-18 - 2013-07-19 |
| 開催地（和） | 北海道大学 工学部アカデミックラウンジ3 |
| 開催地（英） | Hokkaido Univ. Faculty of Eng. Academic Lounge 3 |
| テーマ（和） | クラウドネットワーク技術、SDN、OpenFlow、プライベートネットワーク（VPN）、オーバーレイネットワーク・P2P、ネットワーク構成技術及び一般 |
| テーマ（英） | Cloud Networking, SDN, OpenFlow, Virtual Private Network (VPN), Overlay Network/P2P, Network configuration, etc. |
| 講演論文情報の詳細 | |
| 申込み研究会 | IN |
| 会議コード | 2013-07-IN-NV |
| 本文の言語 | 日本語 |
| タイトル（和） | 記号実行によるパケットの抽象化を用いたOpenFlowネットワークのモデル検査方式の提案 |
| サブタイトル（和） | |
| タイトル（英） | Model Checking of OpenFlow Network with Abstraction of Packets Based on Symbolic Execution |
| サブタイトル（英） | |
| キーワード(1)（和/英） | Software-Defined Networking / Software-Defined Networking |
| キーワード(2)（和/英） | OpenFlow / OpenFlow |
| キーワード(3)（和/英） | 記号実行 / Symbolic execution |
| キーワード(4)（和/英） | 形式手法 / Formal methods |
| キーワード(5)（和/英） | モデル検査 / Model checking |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 八鍬 豊 / Yutaka Yakuwa / ヤクワ ユタカ |
| 第1著者 所属（和/英） | 日本電気株式会社 (略称： NEC) NEC Corporation (略称： NEC) |
| 第2著者 氏名（和/英/ヨミ） | 富沢 伸行 / Nobuyuki Tomizawa / トミザワ ノブユキ |
| 第2著者 所属（和/英） | 日本電気株式会社 (略称： NEC) NEC Corporation (略称： NEC) |
| 第3著者 氏名（和/英/ヨミ） | 登内 敏夫 / Toshio Tonouchi / トノウチ トシオ |
| 第3著者 所属（和/英） | 日本電気株式会社 (略称： NEC) NEC Corporation (略称： NEC) |
| 講演者 | 第1著者 |
| 発表日時 | 2013-07-19 15:15:00 |
| 発表時間 | 25分 |
| 申込先研究会 | IN |
| 資料番号 | IN2013-54 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | no.140 |
| ページ範囲 | pp.107-112 |
| ページ数 | 6 |
| 発行日 | 2013-07-11 (IN) |
[研究会発表申込システムのトップページに戻る]