FIT2016 第15回情報科学技術フォーラム 開催日:2016年9月7日(水)~9日(金) 会場:富山大学キャンパス
抄録
RC-005
MANETプロトコルのモデル検査のための状態空間削減手法
長島悠太・小島英春・土屋達弘(阪大)
MANETは,端末が自律的に通信することにより構築されるネットワークである.MANETプロトコルに不具合が発生しないかを検証するにあたって,モデル検査が有用である.しかし端末数の増加に伴い,トポロジ数が大きく増加し,容易に状態爆発が生じる.本論文では,MANETプロトコルの1つであるAODVを対象にし,その経路構築のモデル検査を行う.端末の持つ経路表のエントリに注目し1回の経路構築のみをモデル検査することにより状態数を削減する手法を提案する.提案手法によりMANETプロトコルのモデル検査を行い,3回の経路構築を1度にモデル検査する場合と比較して,状態数やメモリ使用量が削減されることを示す.