抽象モデル検査とその応用

2000 年度 実績報告書

• 研究課題/領域番号: 11480062
• 研究機関: 東京大学
• 研究代表者: 萩谷 昌己 東京大学, 大学院・理学系研究科, 教授 (30156252)
• 研究分担者: 山本 光晴 千葉大学, 理学部, 助手 (00291295) ; 高橋 孝一 産業技術総合研究所, 主任研究員 ; 玉井 哲雄 東京大学, 大学院・総合文化研究科, 教授 (60217172)
• キーワード: 検証 / モデル検査 / 抽象解釈 / 定理証明 / グラフ探索 / 並行ゴミ集め / セキュリティ

研究概要

本年度の主な成果は以下の通りである。
抽象モデル検査の手法に関しては、昨年度より正則表現を用いてリンク構造を抽象化する手法の研究を行っている。今年度もこの研究を進め論文としてまとめた。
抽象モデル検査の応用として、昨年度よりセキュリティ・プロトコルの検証のためのnonce解析の研究を行っているが、本年度はnonce解析の手法とstrand空間に基づく検証手法を結び付けることにより、Needham-Schroederなどのセキュリティ・プロトコル(認証プロトコル)を極めて簡潔に検証できることを示した。両者とも状態や状態遷移列を抽象化することによって解析を行っている。
セキュリティ・プロトコルの検証に関しては、侵入者による攻撃が確率的に成功する場合の解析についても検討を行った。攻撃手順に成功確率が対応するので、最大確率の攻撃手順を探索するアルゴリズムが必要になる。しかも、攻撃の成功確率は計算時間に依存し、プロトコル中に設定されたタイムアウト時間内に計算が終了しなければならない。現在、timed automataを用いてこのような問題の定式化を試みている。timed automataの検証にはregion解析などの抽象モデル検査の手法が必要であり、これにさらに最大確率(ある種の最短経路)を計算するアルゴリズムを加味しなければならない。
モデル検査を用いたアルゴリズムの探索に関しては、BDD (binary decision diagram)を用いた探索手法に関する実験を行った。アルゴリズムの空間をパラメータの入ったテンプレートによって定義し、BDDによる記号的なモデル検査を用いてテンプレートの検証を行う。すると、一回の検証によってテンプレートの中のパラメータに関する制約条件を求めることができる。ケース・スタディとして同期アルゴリズムの探索を行った。探索空間を小さくするためのBDDを近似(抽象化)する試みも行った。
モデル検査アルゴリズムの検証に関しては、昨年度に引続き、ノード間に抽象化関係が導入された場合のグラフ探索アルゴリズムの定式化と検証の研究を行っているが、今年度もこの研究を進め論文としてまとめた。また、モデル検査において最も基本的である到達可能性の計算における状態の抽象化と、正例からの学習問題を関連付ける研究も行った。

研究成果

• [文献書誌] 高橋孝一,萩谷昌己: "正則表現を用いた並列ごみ集めの抽象モデル検査"情報処理学会論文誌プログラミング. Vol.42 No.SIG2(PRO9). 61-70 (2001)
• [文献書誌] 山本光晴,高橋孝一,萩谷昌己,西崎真也,玉井哲雄: "グラフ探索アルゴリズムの発展とその検証"コンピュータソフトウェア別冊ソフトウェア発展. 92-108 (2000)
• [文献書誌] Masami Hagiya,Koichi Takahashi: "Discovery and Deduction"Discovery Science, Lecture Notes in Artificial Intelligence. 1967. 17-37 (2000)
• [文献書誌] Koichi Takahashi,Masami Hagiya: "Abstraction of Link Structures by Regular Expressions and Abstract Model Checking of Conccurrent Garbage Collection"First Asian Workshop on Programming Languages and Systems. 1-8 (2000)
• [文献書誌] 高橋孝一,戸田洋三,萩谷昌己: "ノンス解析とストランド空間モデル"日本ソフトウェア科学会第17回大会論文集. (2000)
• [文献書誌] 萩谷昌己,高橋孝一: "証明の表現"夏のプログラミング・シンポジウム「計算機と表現」報告集. 89-92 (2001)