研究実績の概要 |
本研究は,モデル検査を行うにあたって,モデル検査の問題点である状態爆発を抑制するために,トポロジの同型判定を利用した状態数削減手法を用いて複数の状態を等価なものとして扱う方法を開発,さらに,状態を等価と扱う際に署名も等価であることを示すことで署名の正しさも検証する手法を開発することである.その進め方は,1:状態数抑制手法を進め,AODVやDSRなどに適用したのちに2:署名に関する研究開発を進め,ISDSR など経路保証プロトコルを対象にする予定である.現時点では,モデル検査器SPINを対象に,1:の状態数削減手法を進めるにあたり,トポロジの同型判定を利用した状態数削減手法を用いて進めており,研究会において発表を行った[1][2].AODVをSPINで用いるモデル言語であるPromelaを用いて実装し,その実装に対して状態数削減手法適用の基本的な考え方や実装方法について述べている.現時点では,状態数削減手法を実装するにあたって,SPINのソースコードの解析やSPINによって出力されるモデル検査を行うC言語のソースコードの解析を行い,手法の実装を進めている. [1] 小島英春, 矢内直人, 経路保証プロトコルを対象にしたSPIN を用いたモデル検査にむけて, 第16回電子情報通信学会ネットワークソフトウェア研究会, 2018 [2]小島英春, 矢内直人, アドホックネットワークプロトコルのモデル検査における状態数削減手法, 第18回電子情報通信学会ネットワークソフトウエア研究会予稿集, 2019.
|