| 研究課題/領域番号 |
16016241
|
|---|
| 研究種目 |
特定領域研究
|
| 配分区分 | 補助金 |
|---|
| 審査区分 |
理工系
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
小川 瑞史 北陸先端科学技術大学院大学, 安心電子社会研究センター, 特任教授 (40362024)
|
|---|
| 研究期間 (年度) |
2004 – 2005
|
| 研究課題ステータス |
完了 (2005年度)
|
| 配分額 *注記 |
3,600千円 (直接経費: 3,600千円)
2005年度: 1,500千円 (直接経費: 1,500千円)
2004年度: 2,100千円 (直接経費: 2,100千円)
|
|---|
| キーワード | モデル検査 / プログラム解析 / 組み合わせ理論 / 代数的データ構造 / フローグラフ / グラフ / 代数的表現 / セキュリティモデル |
|---|
| 研究概要 |
近年、モデル検査の実装技術の発達とハードウェアの進歩により、「プログラム解析=抽象化+モデル検査」というパラダイムが現実的なものとなっている。たとえば、既存のモデル検査系SMVを、Javaを中間言語Jimpleへ変換する言語処理環境SOOTと組み合わせることで、簡単にプログラム解析を実装することが可能である。これは小〜中規模のプログラムに対して有効であるが、処理時間がサイズとともに急速に増大し、大規模プログラムの解析をどう行うかは、現在ホットな研究領域である。この処理時間増大の原因の一つは、モデル検査などで標準的なアルゴリズムが収束するまで何度も反復してプログラム全体を追跡するためである。
本研究では、実際のプログラムのフローグラフは比較的良い構造をもっているという観察に基づき、モデル検査のアルゴリズムから見直しをはかることで、大規模なプログラムへの適用可能性を探ることを提案した。具体的には、
(1)組み合わせ理論の成果を用いて、すでに提案してきたグラフの代数的データ構造(SP項)に基づき、反復がなく効率の良いアルゴリズムおよびその理論的基礎の確立、
(2)実用的な問題におけるケーススタディによる問題点の明確化
について研究を行った。
|
