| 研究課題/領域番号 |
26540026
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥治 名古屋大学, 情報科学研究科, 教授 (70230612)
|
|---|
| 研究協力者 |
李 国強 上海交通大学, ソフトウェア学院, 准教授
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| 研究課題ステータス |
完了 (2016年度)
|
| 配分額 *注記 |
3,380千円 (直接経費: 2,600千円、間接経費: 780千円)
2016年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2015年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2014年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
|---|
| キーワード | 実時間性 / ソフトウェア検証 / 並行プログラム / 実時間プログラム / 関数型言語 / ハイブリッドシステム / プログラミング言語 / 実時間処理 / コード証明 / 分離論理 / 実時間性検証 / スーパーバイザ制御 / Nested Timed Automaton |
|---|
| 研究成果の概要 |
本研究では、実時間性を持つ並行プログラムに対する証明に基づいた検証技法を与える。以下の３つの観点から研究を実施した。(1) コード証明：オープンソースのToppers RTOSの最小モデルであるSSPカーネルのソースコードに対して分離論理によるコードの証明を行った。ビットマップによる優先度フラグの操作が正しく行われることを示した。(2)実時間プログラムの実行モデルとなるNested Timed Automataのエラー到達可能性検査技法を研究した。(3) 関数型言語のDSLであるYampaに対して離散的に実行する場合の動作意味を与えた。
|
