| 研究概要 |
本年度の主な成果は以下の通りである。
並列ゴミ集めの検証のためにヒープを抽象化する方法に関しては,昨年度に引続き,証明支援系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に適用することにより,効率のよりよい探索アルゴリズムを得ることができた.
以上の他にも,抽象モデル検査に関連した研究を進めた.
|
