| 研究課題/領域番号 |
25280023
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 一部基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥治 名古屋大学, 情報科学研究科, 教授 (70230612)
|
|---|
| 研究分担者 |
寺内 多智弘 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
|
|---|
| 研究協力者 |
李 国強 上海交通大学, ソフトウェア学院, 准教授
今井 敬語 有限会社 : ITプラニング
ウリドフスキー イレック レスター大学, 情報学部, 准教授
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| キーワード | 実時間システム / 到達可能性解析 / プッシュダウンシステム / クロック凍結 |
|---|
| 研究成果の概要 |
本研究では、再帰呼び出しや割り込みなどの手続き呼び出しを持つ高レベル言語で記述された実時間プログラムの振舞いをモデル化するNested Timed Automaton(以下NeTA)を提案し、到達可能性が決定可能であることを示し、安全性検証が可能であることを示した。NeTAは、時間オートマトンをスタックアルファベットに持つプッシュダウンシステムである。さらに、時間オートマトンがスタック上にあるときにクロックを凍結する機構を導入しても、一定の条件のもとで到達可能性が保存することを示した。さらに、効率的なゾーン構成による検証手法について検討した。
|
| 自由記述の分野 |
並行計算モデル
|
