2013 Fiscal Year Annual Research Report
高レベル言語で記述されたリアクティブシステムに対する実時間性質の検証
| Project/Area Number |
25280023
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
結縁 祥治 名古屋大学, 情報科学研究科, 教授 (70230612)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
寺内 多智弘 名古屋大学, 情報科学研究科, 准教授 (70447150)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | 実時間プログラム / 関数型プログラム / プッシュダウンシステム / 時間オートマトン |
|---|
| Research Abstract |
平成25年度は、実時間システムに対する基本的な計算モデルとしてNested Timed Automaton(NeTA)について重点的に研究を行った。
NeTAは、スタックアルファベットとして時間オートマトンに拡張したPushdown Systemであり、スタックを持つ実時間プログラムをモデル化することを目的とする。時間に依存した振舞いをもつプログラムの呼出しは、スタックアルファベットである時間オートマトンをPush操作、プログラム終了によってもとのプログラムへのリターンをPop操作によってモデル化する。各プログラムは局所的な時間経過に依存して動作する。呼出しレベルには制限がないため、NeTAは従来の時間オートマトンを拡張した枠組みである。NeTAの特徴は、スタックに格納された時間オートマトンのクロック変数が時間経過とともに増加することである。これは、実際のプログラムの実行においてもスタック上において時間経過は有効であることに対応している。研究開始前にNeTAは、既存研究で提案されていDTPDA(Dense-timedPushdown Automaton)の到達可能性において同等の性質をもつことが予想されていたが、NeTAをDTPDAに変換する手法を示し、NeTAが実時間システムのモデルとして有用であることを示した。
この他に、時間に依存したシステムをモデル化するハイブリッドシステムの解析技法としての無限小数を導入したプログラム検証の実例、形式手法のAlloyに実数を導入した体系の拡張と検証手法の検討を行った。これらの研究では、既存のツールを時間に依存するプログラムに適用する手法について主に検討した。さらに、高階関数プログラムの停止性についての研究を実施し、高階関数プログラムに対する検証手法の拡張をおこない、研究結果を国際会議ESOPで発表する予定である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
基本モデルとしてのNeTAに対して国際会議で研究発表を行い、その他時間に依存するプログラムの検証方法についての研究を行った。さらに、高階関数プログラムの停止性についての検証手法についても新たな結果を得た。
検証ツールの構築については、従来の検証ツールを利用して時間に依存したプログラム検証を試みた。NeTAの結果は研究開始前に検討していた結果であり、さらに証明方法を検討して国際会議で発表を行った。公表したDTPDAへの変換による到達可能性検証以外にも、WSTS(Well structured transition systems)を用いた検証方法についても検討し、以後の研究で計算モデルの発展と検証手法についても展望が得られており、ほぼ予想どおりに研究は進展していると判断している。
|
| Strategy for Future Research Activity |
今後は、２５年度に提案したモデルにより実現に近い実時間プログラムを対応づけることによって、リアクティブ性をもつ実時間プログラムの検証手法、ならびに、具体的な検証ツールの適用についての研究を進める。検証ツールは新たにツールを構築するよりも、既存のSMTソルバーやモデル検査ツールを組み合わせることで実用的な検証が可能であることを示す。さらに、検証したモデルから振舞いが検証された実時間プログラムの構成についても検討を進める。２５年度に購入したサーバーを利用して、様々な例に対して手法を適用して有効性について研究を進める。
海外共同研究者や日本の他大学の研究者とともに、時間プログラムの検証のためのモデルとしてWSTS(Well structured Transition System)を研究し、効率のより検証手法について研究をすすめる計画である。
|
| Expenditure Plans for the Next FY Research Funding |
旅費および人件費が見込みよりも使用額が少なかった。物品については、必要とする性能を持つ物品が予定より安価に調達できたことによる。
研究の進行を加速し、より高性能の計算資源が有効に活用できるように、計算機およびファイルサーバーの整備をすすめる。また、積極的に学会発表を行うことを目指す。
|
-
-
-
-
-
-
-
-
[Presentation] Nested Timed Automata2014
Author(s)
Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen
Organizer
第16回プログラミングおよびプログラミング言語ワークショップ
Place of Presentation
熊本県阿蘇
Year and Date
20140307-20140309
-
-
