2004 Fiscal Year Annual Research Report
| Project/Area Number |
16016241
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 特任教授 (40362024)
|
|---|
| Keywords | プログラム解析 / 組み合わせ理論 / グラフ / 代数的表現 / モデル検査 / セキュリティモデル |
|---|
| Research Abstract |
本研究計画は,リーズナブルなコストでの大規模プログラムの信頼性向上を目的として,バグのもととなる様々な変則性を検出する複数のプログラム解析を自動生成し,漸近的にプログラムの信頼性を高める手法の提案を目指している.具体的には,
(1)組み合わせ理論の成果を用いて,すでに提案してきたグラフの代数的データ構造(SP項)に基づき反復がなく効率の良いアルゴリズムおよびその理論的基礎の確立.
(2)実用的な問題におけるケーススタディによる問題点の明確化.
の2点の研究をすすめている.特に前者については「プログラム解析=抽象化+モデル検査」のパラダイムを想定しているが,標準的なモデル検査を超えたプッシュダウンモデル検査に焦点をおいている.
H16年度は,(1)については,a.SP項の完全な公理化,およびb.SP項によるプログラム解析記述のケーススタディの二点について研究をすすめた.a.については,木幅を制限しないグラフの完全な公理化を提案した(この公理化は無限個の関数記号と公理からなる,国際会議FLOPS04採録・発表).現在,木幅を制限した場合の完全な公理化(有限個の関数記号と公理からなる)について研究を進めている.b.については,古典的なプログラム解析はほとんどネストしないUNTILオペレータで記述できることに注目して,不要引数・定数伝播・コードモーションを例としたUNTILオペレータのSP項による表現を提案した(ワークショップWNASC2004にて口頭発表).
(2)については,a.NTTの開発する時刻認証(イベント順序証明)システムのセキュリティモデルの諸性質の形式的証明,b.グリッド計算におけるセキュリティモデルの提案,c.関数型プログラムの解析のプッシュダウンモデル検査による実装の検討を行った.a.は,Merkle木のインクリメンタルな構成法における完全化可能性とサンティ検査の正当性について定理照明系を用いて示した.b.はグリッド計算におけるdelegationなどを効率的に実行するためのセキュリティモデルを提案した(国内誌コンピュータソフトウェア採録,国際会議PDCAT04採録・発表).現在,モデル検査による検証法を検討中である.
|
