| 研究概要 |
本課題は、抽象モデル検査を中心に,計算システムの検証方法に関して研究を行った.以下はその主な結果である.
まず、並行ゴミ集めなど,ヒープを扱うアルゴリズムを検証するために,ヒープ構造を抽象化する一般的な方法を提案した。ヒープ上のセル間の関係を表現するために、セルから前方および後方への連結状況を特徴づける正則表現を用いる方法を考案した。
抽象モデル検査の応用としては、セキュリティ・プロトコルの検証のために,nonce解析(nonceの漏洩の可能性の解析)を提案し,これとstrand空間に基づく検証手法を結びつけた.また,確率的な攻撃やdenial of serviceに対する解析を行うために,時間付き集合書き換え(timed multiset rewriting)の体系を提案し,その解析技術に関する研究を進めた.
モデル検査を用いたアルゴリズムの探索に関しては、並行ゴミ集めのためのon-the-flyとその二つの変種、snapshoptとその変種を発見した。また、相互排除のためのアルゴリズムの発見を試み,特殊な状況におけるDekkerのアルゴリズムの変種を発見した。さらに,BDD (binary decision diagram)を用いて探索を高速化する試みを行った.
モデル検査アルゴリズム自身の検証に関しては、グラフのノード間に抽象化関係を導入することにより、covering graph constructionなどの抽象モデル検査のアルゴリズムを包含する枠組を定式化した。以上の結果を,timedautomatonの検証に適用した.特に,コスト概念の入ったtimed automatonであるpriced timed automatonに対して,コスト最小の状態遷移経路を探索するアルゴリズムを,本研究で提案した抽象アルゴリズムの具体例として定式化した.さらに,抽象アルゴリズムのA*バージョンを定式化し,それをprimed-timed automatonに適用した.
|
