2016 Fiscal Year Annual Research Report
Verification of real-time reactive systems in high-level programming languages
| 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 |
本年度は、前年度の引き続いて実時間プログラムの高度化モデルとしての時間プッシュダウンシステムの状態到達性に関する研究を進めた。既存研究に対してクロック凍結機能を加えて前年度までに得られたWSPDS(Well Structured Push Down System)のコーディングにもとづいて領域解析に基づく解析エンコーディングを進めた。クロック凍結機構は、実時間プログラムの振舞いにおいて、実時間プログラムがクロックを管理する場合のモデル化として適しており、手続き呼び出しが割込みによって中断された場合に手続き呼び出し中に確保すべき時間をモデル化することができるため、より正確に実時間プログラムの振舞いをモデル化することが可能になった。このような拡張されたモデルにおいて、大域的なクロックを１個に制限すると到達可能性の決定可能性が保存され、２個以上の場合には決定性が保証されないことが示された。大域的なクロックが決定可能性について１個に制限されるという結果は、実時間プログラムの検証可能性に対する限界を示しており、高度化の理論的な限界を示している。今年度はさらに、実用的なツールのモデル化としてゾーン検証手法についての検討を進めた。ゾーン検証はより効率的に振舞いをモデル化することが期待でき、今後の実時間性を持つプログラムの検証手法として利用することが期待できる。本研究は、理論研究を基本とした実用的な検証手法の構築を目標としており、この点において基本的な結果が得られたと考えており、今後は、モデルの最適化と効率的な検証手法をさらに開発し、実用化を目指した研究を進めていく必要がある。
|
| Research Progress Status |
28年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
28年度が最終年度であるため、記入しない。
|
| Causes of Carryover |
28年度が最終年度であるため、記入しない。
|
| Expenditure Plan for Carryover Budget |
28年度が最終年度であるため、記入しない。
|
