2009 Fiscal Year Annual Research Report
マルチスレッド再帰プログラムの自動検証のための形式モデル
| Project/Area Number |
21700045
|
|---|
| Research Institution | Kochi University of Technology |
|---|
Principal Investigator |
高田 喜朗 高知工科大学, 工学部, 准教授 (60294279)
|
|---|
| Keywords | 形式的検証 / 形式言語理論 / モデル検査 / マルチスレッド / プッシュダウンシステム |
|---|
| Research Abstract |
現在普及している有限状態モデルに基づくモデル検査ツールでは,システムの振る舞いを有限状態モデルに近似する必要があり,そのために検証に失敗する場合が生じる.これに対し,プッシュダウンシステム(PDS)などの無限状態モデルを用いることで,システムの振る舞いをより正確に表現することが可能となる.しかし,これまでのPDSに基づくモデル検査法では,複数のスレッドが並行動作するマルチスレッドプログラムをうまく扱うことができなかった.並行動作する有限状態モデルの合成が有限状態モデルで表現できるのに対し,PDSの並行合成は一般にはTuring機械と等価となるため,有用な検証は行えない.そのため,検証に必要な機能を抽出したモデル化が重要となる.現在,多重文脈自由文法,インデクス文法などの形式文法との関連,および,プロセス代数との関連を中心に調査し,基本モデルを検討中である.また,再帰プログラムの形式モデル化に関連して,与えられたセキュリティ仕様を満たすようにプログラム中にアクセス権検査文を挿入する問題について考察し,モデル検査法を基盤として問題の枠組を提案した.また,この問題が補NP困難であることを示すとともに,現実的な入力例に対して効率よく動作するアルゴリズムを考案し,試作システムによる評価を行った.
|
