モデル検査を用いたタグVLANの設定検査

• Item type: Journal(1)
• 公開日: 2006-07-15
• タイトル: モデル検査を用いたタグVLANの設定検査
• タイトル / 言語: en
• タイトル: Model Checking Configurations for Tag VLAN
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: ネットワークサービス基礎
• 著者所属: 日本電信電話株式会社NTTコミュニケーション科学基礎研究所
• 著者所属(英): en
• 著者所属(英): NTT Communication Science Laboratories, NTT Corporation
• 著者名: 櫻田, 英樹
• 著者名(英): Hideki, Sakurada
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: ネットワーク機器の設定は通常人手によって行われる． このため，通信の断絶や情報の漏曳などネットワークに深刻な障害をもたらす 設定ミスが発生することがある．本稿ではネットワーク機器，特にタグVLANを用いるEthernet機器の設定の正しさを モデル検査法を用いて検査する方法を提案する． この方法により，ネットワークに要求される様々な性質を効率的に 検査できるようなる．また，設定に誤りがある場合には，この方法により起こりうる可能性のある障害について 調べることができる．これは設定ミスを修正する際に便利である．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Network nodes such as switches, routers, and terminals are usually configured by network engineers' hands. Even experienced network engineers sometimes make mistakes that may cause serious troubles such as packet loss or leakage of credential information to unexpected third-party. In this paper, we propose a method for verifying configurations of nodes on Ethernet LAN where VLAN-tagging is used. The method is based on model-checking, one of the most widely used formal verification techniques. It enables us to efficiently verify various properties about networks. Moreover, it enables us to find possible troubles in case configuration mistakes exist. They are useful in fixing the configurations.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 47, 号 7, p. 2247-2257, 発行日 2006-07-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764