| 研究課題/領域番号 |
24500032
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
萩原 茂樹 東京工業大学, 情報理工学(系)研究科, 助教 (70334547)
|
|---|
| 研究協力者 |
島川 昌也 東京工業大学, 大学院情報理工学研究科, 研究員 (00749161)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| 研究課題ステータス |
完了 (2014年度)
|
| 配分額 *注記 |
4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2014年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2013年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
2012年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | 形式手法 / 組み込みシステム仕様 / 修正情報抽出 / 時間論理 / オートマトン / 極小充足不能集合 / 組込みシステム仕様 |
|---|
| 研究成果の概要 |
組み込みシステムの仕様を記述する際、一度に誤りなく記述するのは困難であるため、誤りのある仕様から修正に有益な情報を得たい。本研究では、誤りのある仕様から、その原因と箇所を表す情報を計算する方法を形式手法により構成した。その計算手法では、仕様を満たす振る舞いを表すωオートマトンにおいてグラフ操作を行なうことで欠陥原因と箇所の情報の計算する。ωオートマトンを簡便に簡約する新しい技術を構成し、解析を効率化しただけでなく、計算する修正情報の形に工夫を加え、現実規模の仕様に適用可能とした。本手法の正当性を証明し、計算量を特定した。さらに、本手法をツールとして実装した。
|
