経路保証プロトコルのモデル検査手法の開発

2021 Fiscal Year Research-status Report

• Project/Area Number: 18K11262
• Research Institution: Osaka University
• Principal Investigator: 小島 英春 大阪大学, 情報科学研究科, 助教 (90610949)
• Co-Investigator(Kenkyū-buntansha): 矢内 直人 大阪大学, 情報科学研究科, 准教授 (30737896)
• Project Period (FY): 2018-04-01 – 2023-03-31
• Keywords: モデル検査 / 状態爆発抑制 / 経路保証プロトコル / 無線マルチホッププロトコル

Outline of Annual Research Achievements

IoT技術の発展によって様々な種類の機器が無線を用いてネットワークに参加することが考えられる．その際に機器間の通信を行うために，通信経路を構築する必要がある．この経路構築を行うためのプロトコルはさまざまあるが，本研究では，構築する経路を保証するプロトコルを対象としている．経路保証プロトコルは，経路構築にあたって署名を用いて構築する経路の正しさを保証するものである．
本研究では，このプロトコルを対象にモデル検査を用いて形式的に経路構築が正しく行われることを示す手法の開発を行っている．ネットワークに存在する端末数が増加すると，それに伴いモデル検査を行うために必要な状態空間が爆発するため，計算時間の増加や検証時の主記憶領域の枯渇により検証が困難になる．そのため，効率的な検証手法の開発が必要となり，本研究では，これまでその手法の開発をおこなってきた．これまでの研究では，状態爆発の抑制手法や経路保証プロトコルの１つであるISDSRへの適用をおこなってきており，それらの手法が状態数を抑制することが可能であることを示してきた．
2021年度では，2020年度までに行ってきた研究をまとめ，論文誌に投稿する予定でいたが，
前年度と同様にコロナ関連の対策に多くの時間を費やしてしまい，進める予定であった内容を進めることができなかったことが，進捗が見られなかった原因と考えている．コロナ対策関連については，2021年度でおおよその対応が終わったと考えられるため，今後，本研究を積極的に進める．

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

2020年度に引き続き，2021年度もコロナ対策関連に多くの時間を費やす必要があり，本研究の進捗は芳しくなかった．しかし，2022年度に向けて，論文を投稿する準備は進めており，これまでの研究をまとめて論文誌に投稿する予定である．

Strategy for Future Research Activity

本研究では，当初の目標として，トポロジに注目した状態数抑制手法を開発し，AODVやDSRなどの既存のアドホックネットワークプロトコルに適用し，状態数削減の効果が得られることを示すこと，ISDSRなどの経路保証プロトコルに開発した状態抑制手法を適用し状態数の抑制効果が得られることを示すことをおこなってきた．今後は，これらをまとめ論文誌へ投稿する予定である．

Causes of Carryover

2021年度に投稿予定であった論文がずれ込んだことにより，2021年度中に利用する予定であった掲載料を利用することができなかった．2022年度では，論文誌へ投稿し，掲載料として利用する予定である．