| 研究課題/領域番号 |
17K17763
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
計算機システム
ソフトウェア
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
冨田 尭 北陸先端科学技術大学院大学, 情報社会基盤研究センター, 講師 (80749226)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2023-03-31
|
| 研究課題ステータス |
完了 (2022年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2019年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2018年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2017年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | ソフトウェア工学 / ソフトウェア検証 / 形式手法 / 協調的リアクティブシステム / 実現可能性 / 自動合成 / 協調的リテクティブシステム |
|---|
| 研究成果の概要 |
本研究では仕様の実現可能性必要条件に基づき協調的リアクティブシステムを自動合成する手法の開発に取り組んだ．
新たに8つの必要条件群を発見し，既知の必要条件群も含めた統一的な特徴付けと階層定理群を与えた．これらの必要条件群は網羅性，保存性，安定性及び戦略化可能性の4つの観点から体系的に分類でき，その観点から仕様の欠陥についての分析と，協調が発生し得ることを導出できる．そして，必要条件群の特性について，判定手続きを構成するサブルーチンの共通性及び類似性からも分析するとともに各必要条件判定の期待計算量を導出し，実現可能性必要条件に基づく協調的リアクティブシステム自動合成手法の基礎を確立した．
|
| 研究成果の学術的意義や社会的意義 |
本研究成果は，より現実的・一般的な自動合成技術の基盤を与えたという点で学術的・社会的な意義がある．
古典的なリアクティブシステム自動合成では敵対的な環境を想定するという過度に厳しい安全性に基づいていたが，本研究では協調の発生を想定し緩和された安全性に基づく自動合成に注目し，合成可能性の基盤となる実現可能性必要条件群について分析した．その結果，実現可能性必要条件群の判定手続きの期待計算量は大きいものの，体系的な特徴付け・分類により，要求仕様の欠陥や協調不調についてのより詳細な分析が可能なことが明らかになったため，仕様修正の容易化を期待できる．
|
