| 研究課題/領域番号 |
16K00092
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 公立千歳科学技術大学 (2019-2021)
東北公益文科大学 (2017-2018)
東京工業大学 (2016) |
|---|
研究代表者 |
萩原 茂樹 公立千歳科学技術大学, 理工学部, 准教授 (70334547)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2022-03-31
|
| キーワード | 形式手法 / 組み込みシステム / 自動合成 / 時間論理 / 検証 |
|---|
| 研究成果の概要 |
組み込みシステムは、機能要件などの定性的制約だけでなく、性能要件などの定量的制約を満たすことが強く望まれ、これら制約を必ず満たすシステムを構成する手法が必要不可欠である。厳密な保証が可能な形式手法により、これらの制約を満たす現実的なシステムを合成するための基礎技術を構成した。具体的には、性能要件をできるだけ満たすシステムの合成手法や、現実規模のシステム構成のためのモジュール分割方法などを構成した。
|
| 自由記述の分野 |
ソフトウェア
|
| 研究成果の学術的意義や社会的意義 |
現実的な仕様からシステムを系統的に構成する手法の研究は、ソフトウェア工学の分野で盛んに行われてきたが、それらはデータオリエンテッドな対応であり、それらから得られるのは「経験則」であると指摘されてきた。「法則」を得る方法として形式手法が注目されている。これまで形式手法は、解析に要する計算量の膨大さにより、現実規模の仕様に適用するのが困難であった。本研究は現実規模の仕様に対して、形式手法で解析が可能な範囲、即ち「法則」が適用可能な範囲を明確にするという学術的な特色がある。
|
