| 研究課題/領域番号 |
18K11262
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60060:情報ネットワーク関連
|
|---|
| 研究機関 | 大阪工業大学 (2022)
大阪大学 (2018-2021) |
|---|
研究代表者 |
小島 英春 大阪工業大学, 情報科学部, 准教授 (90610949)
|
|---|
| 研究分担者 |
矢内 直人 大阪大学, 大学院情報科学研究科, 准教授 (30737896)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2020年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2019年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2018年度: 2,210千円 (直接経費: 1,700千円、間接経費: 510千円)
|
|---|
| キーワード | モデル検査 / 状態爆発抑制 / 経路保証プロトコル / 無線マルチホッププロトコル / 形式検証 |
|---|
| 研究成果の概要 |
本研究では，センサネットワークやアドホックネットワークで利用される経路保証プロトコルの形式検証を行う際に生じる状態爆発を抑制する手法の開発を行なった．基本的な考え方は，同じトポロジ形状であれば等価な状態とみなすことで走査する状態数を削減することである．また，対象とする経路保証プロトコルは，署名を用いて経路の正しさを保証するため，開発手法では，同じトポロジ形状であり等価な状態とみなしたトポロジであればそれぞれの署名も等価であるとみなす方法を組み込んでいる．この手法をモデル検査器SPINに適用し，経路保証プロトコルの検証を行ない，状態数が削減されること，実行時間の短縮を示すことができた．
|
| 研究成果の学術的意義や社会的意義 |
センサネットワークやアドホックネットワークが社会で展開されることを考えると，経路が構築されること，情報の通信経路が信頼できることが重要である．経路保障プロトコルは，それらを実現するものである．これを用いるにあたって，正しく動作するかどうかを事前に検証することが必要である．従来の方法では，状態爆発により検証の完了が困難である場合があることや検証に必要な実行時間が長くなることがあるが，本研究で開発した手法を用いて状態爆発を抑制することで，検証に必要な時間を削減することが可能となった．
|
