| 研究課題/領域番号 |
25280023
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥治 名古屋大学, 情報科学研究科, 教授 (70230612)
|
|---|
| 研究分担者 |
寺内 多智弘 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| キーワード | 実時間性 / プログラム検証 / 関数型言語 / 到達可能性解析 |
|---|
| 研究実績の概要 |
本年度は、昨年度に引き続いて実時間プログラムのモデルとしてプッシュダウンオートマトンを基礎とするNested Timed Automataの到達可能性問題に定式化、特に、時間を値として扱うためのクロック凍結機能についての研究、さらに、高階関数型言語におけるプログラム解析手法についての研究を行った。
Nested Timed Automataは、実時間性を持つプログラムコードの実行をモデル化する。従来からの研究によって、クロックが停止しない場合は状態到達可能性が決定可能であることを示した。クロックの値を文脈を切り替えるタイミングで保存する機能を追加することで、クロック変数の値を保存するモデルの拡張を提案した。クロック値を保存するメカニズムをスタック操作時に限定することで、状態到達可能性が決定可能であることが示された。ここで、大域的なクロック変数を導入してクロック変数間の値代入を許す場合について、クロック変数の数が１個であれば到達可能性は決定可能、２個以上の場合は決定不能であることが示された。このことから、実時間性をもつプログラムの検証可能性についての基本的な結果が得られた。
高階関数型言語におけるプログラム解析手法については、CEGAR手法を用いた安全性解析および活性検証の手法を拡張して実用的な検証手法を示した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
実時間プログラムのモデルとして研究している時間オートマトンをプッシュダウンに拡張したモデルにおいて、状態の到達可能性を示すことができたのは大きな成果である。この成果から再帰構造をもつ一般的なプログラムに対して検証可能なクラスが比較的精度よくモデル化できることを示すことができた。高階の概念の取り込みについては、これらの成果をもとにプログラミング言語にとりこむ。Haskellなどの具体的なプログラミング言語に時間の概念が導入されているFunctional Reactive Programmingの概念をもとにして、検証を行う際の基礎となる。高階言語における検証については、CEGAR技法に基づいてプログラムの活性を保証する適切な型を推論する手法を示した。
|
| 今後の研究の推進方策 |
最終年度は、これまでの理論的な研究をさらに進めるとともに、具体的なプログラミング言語を対象とした研究を進める。理論的研究については、高階関数型言語における型推論のさらなる精度の向上、局所クロックの凍結機能を持つ時間プッシュダウンオートマトンの到達可能性解析、さらに、並行性を導入して通信機能を持つプログラムモデルの到達可能性についても解析を進める。
|
| 次年度使用額が生じた理由 |
予定していた航空運賃の費用などが見積もりよりも安価ですんだこと、また、発表についての出張費用が予想より少額であったこと。さらに、学生が実施した研究について企業からの共同研究費用援助が得られたことによる。必要な計算資源が見積もりよりも安価であったことも理由としてあげられる。
|
| 次年度使用額の使用計画 |
今年度は、研究発表や研究集会への参加を予定どおりに行い、主に最終年度の具体的研究結果を示すための費用として利用する計画である。
|
