モデル検査を用いたSDNの経路変更手順生成手法の提案
工学研究科 情報学専攻 博士前期課程2年 RYU TAKEMASA-
背景
ネットワークの柔軟性と安全性を
両立する新たなアプローチ本研究のきっかけは、自動運転技術の安全性向上を目指していたことにあります。完全自動運転の実現には多くの課題があり、その中でも車線変更や経路変更の安全性が重要なテーマでした。そこで、安全性を保証する方法として「モデル検査」に着目し、研究を進める過程でネットワーク制御の分野に応用できる可能性を見出しました。特に、SDN（Software-Defined Networking）の経路変更手順に適用することで、安全性の高いネットワーク管理が実現できるのではないかと考えました。
SDNは、ネットワークの制御をソフトウェアで一括管理できる技術であり、柔軟なネットワーク構成が可能になります。しかし、経路変更の手順が適切でない場合、パケットロスやセキュリティリスクが発生する可能性があります。そこで、本研究では、形式手法の一つである「モデル検査」を用いて、信頼性の高い経路変更手順を生成する手法を提案します。 -
目的
モデル検査を活用し、
信頼性の高い経路変更を実現本研究の目的は、モデル検査を活用して、SDN における経路変更手順の安全性を向上させることです。具体的には、一般的なモデル検査ツール「NuSMV」を用いてネットワークの状態遷移モデルを構築し、期待される性質を満たしているかを検証することで、信頼性の高い安全な経路変更手順を導出します。
-
開発
NuSMVを用いた検証と
状態爆発問題の克服モデル検査ツール「NuSMV」を活用し、SDN の経路変更手順を自動生成する手法を考案しました。この検査ツールでは、モデルが検証対象の性質を満たしているかを判定し、NO の場合には反例が出力されます。この反例の出力を活用して、正しい経路変更手順が反例として出力されるよう判定することで、安全な経路変更手順を導出します。
また、モデル検査の大きな課題の一つである「状態爆発問題」に対処するため、モデルを「ブロック」単位で抽象化する手法を導入しました。これにより、状態数を削減し、状態爆発を抑制しています。 -
検証
データに基づく有効性の確認と
今後の課題実験の結果、提案手法によって、従来手法と比較してブロック数が増加した場合に経路変更の安全性が向上することを確認しました。一方で、ブロック数が少ない場合には従来手法の方が効率的であることも判明し、さらなる最適化が課題として残りました。
研究の進行にあたっては、国内外の関連研究を幅広く調査し、最新の知見を取り入れながら検証を行いました。 -
まとめ・効果
ネットワークの安全性向上と
モデル検査の可能性本研究を通じて、SDN における経路変更の安全性向上に貢献する新たな手法を提案しました。これにより、ネットワークの柔軟性を損なうことなく、パケットロスやセキュリティリスクを低減することが可能となります。
また、モデル検査を用いることで、システムの正当性を数学的に保証することの重要性を実感しました。今後は、提案手法の拡張を行い、より実用的な形での適用を目指します。
本研究を進めるにあたり、関東学院大学の充実した研究環境が大きな支えとなりました。研究室は常に快適で、集中して作業に取り組むことができました。また、教授陣の親身な指導により、専門知識を深めるだけでなく、新しい視点を得る機会にも恵まれました。学内の設備や文献の充実も、研究をスムーズに進めるうえで大きな助けとなりました。関東学院大学だからこそ、自由な発想で研究に取り組み、最適な環境で試行錯誤を繰り返すことができたと実感しています。
SITE CONTENTS
