大規模プログラムのためのプログラム解析の自動生成

Research Project

Project/Area Number	16016241
Research Category	Grant-in-Aid for Scientific Research on Priority Areas
Allocation Type	Single-year Grants
Review Section	Science and Engineering
Research Institution	Japan Advanced Institute of Science and Technology
Principal Investigator	小川瑞史北陸先端科学技術大学院大学, 安心電子社会研究センター, 特任教授 (40362024)
Project Period (FY)	2004 – 2005
Project Status	Completed (Fiscal Year 2005)
Budget Amount *help	¥3,600,000 (Direct Cost: ¥3,600,000) Fiscal Year 2005: ¥1,500,000 (Direct Cost: ¥1,500,000) Fiscal Year 2004: ¥2,100,000 (Direct Cost: ¥2,100,000)
Keywords	モデル検査 / プログラム解析 / 組み合わせ理論 / 代数的データ構造 / フローグラフ / グラフ / 代数的表現 / セキュリティモデル
Research Abstract	近年、モデル検査の実装技術の発達とハードウェアの進歩により、「プログラム解析=抽象化+モデル検査」というパラダイムが現実的なものとなっている。たとえば、既存のモデル検査系SMVを、Javaを中間言語Jimpleへ変換する言語処理環境SOOTと組み合わせることで、簡単にプログラム解析を実装することが可能である。これは小〜中規模のプログラムに対して有効であるが、処理時間がサイズとともに急速に増大し、大規模プログラムの解析をどう行うかは、現在ホットな研究領域である。この処理時間増大の原因の一つは、モデル検査などで標準的なアルゴリズムが収束するまで何度も反復してプログラム全体を追跡するためである。本研究では、実際のプログラムのフローグラフは比較的良い構造をもっているという観察に基づき、モデル検査のアルゴリズムから見直しをはかることで、大規模なプログラムへの適用可能性を探ることを提案した。具体的には、 (1)組み合わせ理論の成果を用いて、すでに提案してきたグラフの代数的データ構造(SP項)に基づき、反復がなく効率の良いアルゴリズムおよびその理論的基礎の確立、 (2)実用的な問題におけるケーススタディによる問題点の明確化について研究を行った。