2014 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 |
本課題の目標は、再帰関数、割り込み、高階関数、オブジェクトなど高度なプログラミング機能を含むリアクティブシステム（外部イベントに対応して動作するプログラム）の検証である。このようなプログラムが本来もつ複雑性に対する検証技術に加えて、実時間性をもつプログラムへの適用技報の確立を目指している。
平成２６年度については、前年度に引き続き、実時間システムとして高階性をもつ計算モデルとしてのNeTA(Nested Timed Automaton)についての研究と、並行して、高階プログラムの停止性研究について行った。NeTAの検証については、一般的に実時間性をもつプログラムの検証における計算複雑さを緩和する手法について検討を行った。NeTAは、時間オートマトンをスタックアルファベットに持つプッシュダウン計算モデルであり、到達可能性をプッシュダウンにおける到達可能性とスタックアルファベット自体の到達可能性に分解して検証する手法について検討した。[LNCS8939] 高階プログラムの検証技法としては、高階関数型言語で記述されたプログラムに対して有効な二項到達可能性解析への帰着による、健全かつ相対的完全な停止性検証の手法を提案した[ESOP 2014]。高レベルプログラムの時相論理仕様検証に対して有効な構成的な検証の枠組みを提案した[CSL-LICS 2014]。この他、並行プログラムの計算モデルにおける逆計算による意味論の詳細化についても研究発表を行った。[LNCS8507]
|
| 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 |
今後は、２６年度に得られた結果を進めてさらに、関数型言語を意図した高階プログラミング言語における停止性に基づいた検証手法、並行して、高階性を持つ実時間計算モデルにおける状態の到達可能性に関する研究を進める。さらに、統計的概念に基づいたより効率的な検証手法についても研究する。これらの統合手法の確立を視野にプロトタイプ的な検証ツールの作成も行う計画である。
|
| Causes of Carryover |
旅費および人件費が見込みよりも使用額が少なかった。物品については、必要とする物品（ファイルサーバーなど）が当初計画よりも安価に彫琢できたことによる。
|
| Expenditure Plan for Carryover Budget |
研究の進行を加速して、検証技法の発展に応じた計算資源を用意するとともに、国外における学会発表を積極的に行うことを目指す。
|
