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