2012 Fiscal Year Annual Research Report
| Project/Area Number |
12J08057
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
佐藤 亮介 東北大学, 大学院・情報科学研究科, 特別研究員(DC2)
|
|---|
| Keywords | 高階関数型言語 / 高階モデル検査 / ソフトウェアモデル検査 / 継続渡し形式変換 / 述語抽象化 |
|---|
| Research Abstract |
高階モデル検査を用いた高階関数型言語のためのソフトウェアモデル検査器の拡張、高速化に関する研究を進め、その成果を論文として発表した。
検証の枠組みの拡張として、既存の高階関数型言語のためのソフトウェアモデル検査器では扱えなかったリストや木構造などの再帰的データ構造、例外処理などを扱えるようにした。例えば,再帰的データ構造を扱えるようにするために、再帰的データ構造に対しても関数によるエンコード法を提案した。これによって再帰的データ構造を用いるプログラムから再帰的データ構造を用いない同じ意味のプログラムへと変換することができる。
検証の枠組みの高速化として、既存の検証の枠組みで用いていた継続渡し形式変換の改良である選択的継続渡し形式変換を提案した。素朴な継続渡し形式変換では、変換後のプログラムが不必要に複雑になり、これによって変換後のプログラムに対して行われる高階モデル検査の計算量が不必要に増えてしまうという問題があった。これを回避するため、なるべく高階モデル検査の計算量が増えないような継続渡し形式変換を提案した。この改良によって高階モデル検査の計算量を抑えることができ、全体の検証時間を短縮することができる。また、別の高速化として、既存の検証の枠組みで用いていた述語抽象化の改良である選択的述語抽象化を提案した。この改良によって、抽象化の精度を上げることができ、全体の検証時間を短縮することができる。
また、この拡張子した検証の枠組みを基に、関数型言語OCamlのサブセットで書かれたプログラムを対象とする検証器を実装した。さらに、検証速度を向上させるためのチューニング等を行った。実装した検証器をさまざまなプログラムに適用し、本手法の有効性を確かめた。
ここまでに得られた成果を国際会議の場で発表し、同時に国外の研究者との意見交換を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画通り、高階モデル検査を用いた関数型言語のためのソフトウェアモデル検査器に関するテーマについて研究を進め、それを実用レベルに近づけるために様々な最適化や拡張を提案することができた.
|
| Strategy for Future Research Activity |
現時点でのソフトウェアモデル検査器では,検証に時間がかかりすぎて実用的なソフトウェアの検証には適用できない。そこで、検証時間のほとんどを占める述語抽象化、および、高階再帰スキームに対するモデル検査のアルゴリズムの改良、高速化を行う。改良したアルゴリズムを用いて、前年度に実装した検証器の改良を行う。その実装を用いて、様々なプログラムに対して複数の性質を検証し、この実装が実用的なものであることを確かめる。
|
