2001 Fiscal Year Annual Research Report
| Project/Area Number |
11480062
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 理学部, 助手 (00291295)
高橋 孝一 産業技術総合研究所, 主任研究員
玉井 哲雄 東京大学, 大学院・情報学環, 教授 (60217172)
|
|---|
| Keywords | 検証 / モデル検査 / 抽象解釈 / 定理証明 / グラフ探索 / 並行ゴミ集め / セキュリティ |
|---|
| Research Abstract |
本年度の主な成果は以下の通りである。
並列ゴミ集めの検証のためにヒープを抽象化する方法に関しては,昨年度に引続き,証明支援系HOLを用いて抽象化の正当性の検証を進めた.具体システムと抽象システムの両方をHOLのもとで定式化し,抽象遷移が具体遷移のsimulationになっていることを形式的に証明した.
昨年度に引続き相互排除アルゴリズムの探索を試みた.BDDを用いた探索の効率化に関しては,BDDの部分木間のハミング距離が閾値よりも小さい場合に,部分木をそれらの選言で置き換えることにより,BDDを近似(抽象化)する試みを行った.
昨年度に引続きセキュリティ・プロトコルを対象とした研究を進めた.今年度は,確率的な攻撃やdenial of serviceに対する解析を行うために,時間付き集合書き換え(timed multiset rewriting)の体系を提案し,その解析技術に関する研究を進めた.特に,クロックの状態の抽象化する技術としてtimed automatonやhybrid automatonに対して確立しているregionの考え方を適用することにより,制限された時間付き集合書き換えにおいて有界性や被覆性が決定可能であることを示した.
セキュリティ・プロトコルの検証については,束縛の概念を用いた認証プロトコルの分類に関する研究を進めた.分類に従って,いくつかの新しいプロトコルを見出すことができた.
昨年度までに行ったグラフ探索アルゴリズムの検証に関する研究を,timed automatonの検証に適用した.特に,コスト概念の入ったtimed automatonであるpriced timed automatonに対して,コスト最小の状態遷移経路を探索するアルゴリズムを,本研究で提案した抽象アルゴリズムの具体例として定式化した.さらに,抽象アルゴリズムのA^*バージョンを定式化し,それをprimed timed automatonに適用することにより,効率のよりよい探索アルゴリズムを得ることができた.
以上の他にも,抽象モデル検査に関連した研究を進めた.
|
-
[Publications] Koichi Takahashi, Masami Hagiya: "Searching for Mutual Exclusion Algorithms using BDDs"Lecture Notes in Computer Science. (出版予定). (2002)
-
[Publications] Yoshiki Kinoshita, Koichi Takahashi: "Cumulatives for Safety"Electric Notes on Theoretical Computer Science. (出版予定). (2002)
-
[Publications] Shin Nakajima, Tetsuo Tamai: "Behavioural Analysis of the Enterprise Java Beans^<TM> Component Architecture"Lecture Notes in Computer Science. 2057. 163-182 (2001)
-
[Publications] Mitsuharu Yamamoto, Masami Hagiya: "Abstract A^* Algorithm and Its Application to Linearly Priced Timed Automata"Proceedings of The Second Asian Workshop on Programming Languages and Systems. 193-205 (2001)
-
[Publications] Masami Hagiya, Mitsuharu Yamamoto, Jean-Marie Cottin: "Symbolic Analysis of Timed Multiset Rewriting and Its Application to Protocol Analysis"Rewriting in Proof and Computation, International Workshop RPC'01. 34-41 (2001)
-
[Publications] 齋藤孝道, 萩谷昌己, 溝口文雄: "公開鍵を用いた認証プロトコルについて"情報処理学会論文誌. 42・8. 2040-2048 (2001)
