2010 Fiscal Year Annual Research Report
マルチスレッド再帰プログラムの自動検証のための形式モデル
| Project/Area Number |
21700045
|
|---|
| Research Institution | Kochi University of Technology |
|---|
Principal Investigator |
高田 喜朗 高知工科大学, 工学部, 准教授 (60294279)
|
|---|
| Keywords | 形式的検証 / 形式言語理論 / モデル検査 / プッシュダウンシステム |
|---|
| Research Abstract |
現在普及している有限状態モデルに基づくモデル検査ツールでは,システムの振る舞いを有限状態モデルに近似する必要があり,そのために検証に失敗する場合が生じる.これに対し,プッシュダウンシステム(PDS)などの無限状態モデルを用いることで,システムの振る舞いをより正確に表現することが可能となる.PDSは再帰プログラムの振る舞いを自然に表現でき,かつモデル検査が可能な無限状態モデルとして知られている.再帰プログラムのPDSによる形式モデル化の応用として,与えられたセキュリティ仕様を満たすようにプログラム中にアクセス権検査文を挿入する問題について考察した.Java仮想機械等に実装されているアクセス権検査機能や,その拡張であるAbadiらの履歴ベースアクセス制御(history-based access control)は,メソッド呼び出しと復帰を基準に許可されるアクセスを決定するものであり,PDSによるモデル化が自然である.本研究ではモデル検査法を基盤としてこの問題の枠組を提案し,到達可能集合の計算を反復することによる不動点計算によってこの問題が解けることを示した.また,生成される到達可能集合の大きさに比例する計算量のアルゴリズムをプロトタイプとして実装し,現実的な入力に対して現実的な時間で適用可能であることを示した.さらに,二分決定図(BDD)等のデータ構造を応用することによるさらなる効率化について基礎的な検討を行った.
|
