2015 Fiscal Year Annual Research Report
高レベル言語で記述されたリアクティブシステムに対する実時間性質の検証
| Project/Area Number |
25280023
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
結縁 祥治 名古屋大学, 情報科学研究科, 教授 (70230612)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
寺内 多智弘 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | 実時間性 / プログラム検証 / 関数型言語 / 到達可能性解析 |
|---|
| Outline of Annual Research Achievements |
本年度は、昨年度に引き続いて実時間プログラムのモデルとしてプッシュダウンオートマトンを基礎とするNested Timed Automataの到達可能性問題に定式化、特に、時間を値として扱うためのクロック凍結機能についての研究、さらに、高階関数型言語におけるプログラム解析手法についての研究を行った。
Nested Timed Automataは、実時間性を持つプログラムコードの実行をモデル化する。従来からの研究によって、クロックが停止しない場合は状態到達可能性が決定可能であることを示した。クロックの値を文脈を切り替えるタイミングで保存する機能を追加することで、クロック変数の値を保存するモデルの拡張を提案した。クロック値を保存するメカニズムをスタック操作時に限定することで、状態到達可能性が決定可能であることが示された。ここで、大域的なクロック変数を導入してクロック変数間の値代入を許す場合について、クロック変数の数が１個であれば到達可能性は決定可能、２個以上の場合は決定不能であることが示された。このことから、実時間性をもつプログラムの検証可能性についての基本的な結果が得られた。
高階関数型言語におけるプログラム解析手法については、CEGAR手法を用いた安全性解析および活性検証の手法を拡張して実用的な検証手法を示した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
実時間プログラムのモデルとして研究している時間オートマトンをプッシュダウンに拡張したモデルにおいて、状態の到達可能性を示すことができたのは大きな成果である。この成果から再帰構造をもつ一般的なプログラムに対して検証可能なクラスが比較的精度よくモデル化できることを示すことができた。高階の概念の取り込みについては、これらの成果をもとにプログラミング言語にとりこむ。Haskellなどの具体的なプログラミング言語に時間の概念が導入されているFunctional Reactive Programmingの概念をもとにして、検証を行う際の基礎となる。高階言語における検証については、CEGAR技法に基づいてプログラムの活性を保証する適切な型を推論する手法を示した。
|
| Strategy for Future Research Activity |
最終年度は、これまでの理論的な研究をさらに進めるとともに、具体的なプログラミング言語を対象とした研究を進める。理論的研究については、高階関数型言語における型推論のさらなる精度の向上、局所クロックの凍結機能を持つ時間プッシュダウンオートマトンの到達可能性解析、さらに、並行性を導入して通信機能を持つプログラムモデルの到達可能性についても解析を進める。
|
| Causes of Carryover |
予定していた航空運賃の費用などが見積もりよりも安価ですんだこと、また、発表についての出張費用が予想より少額であったこと。さらに、学生が実施した研究について企業からの共同研究費用援助が得られたことによる。必要な計算資源が見積もりよりも安価であったことも理由としてあげられる。
|
| Expenditure Plan for Carryover Budget |
今年度は、研究発表や研究集会への参加を予定どおりに行い、主に最終年度の具体的研究結果を示すための費用として利用する計画である。
|
