研究課題/領域番号 |
18K11240
|
研究種目 |
基盤研究(C)
|
配分区分 | 基金 |
応募区分 | 一般 |
審査区分 |
小区分60050:ソフトウェア関連
|
研究機関 | 北陸先端科学技術大学院大学 (2019-2022) 福井大学 (2018) |
研究代表者 |
石井 大輔 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (00454025)
|
研究期間 (年度) |
2018-04-01 – 2023-03-31
|
研究課題ステータス |
完了 (2022年度)
|
配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2021年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
2020年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2019年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2018年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
キーワード | ハイブリッドシステム / 制約プログラミング / 区間解析 / 探索・論理・推論アルゴリズム |
研究成果の概要 |
連続離散ハイブリッドシステム(HS)のための制約プログラミング技術を開発することを目指し,大規模・複雑な組込みシステムをモデリングしたHSに対し,高信頼かつ有用な解析を実施する手法・ツールに関する研究を実施した.制約プログラミング技術に基づき,安全性のモデル検査や目的関数の最適化をする手法・ツールを提案した.提案手法は,SimulinkおよびAcumenで記述したHSを,実数,浮動小数点数,区間等の領域の変数をもつ制約へと符号化し,ソルバーによる解析を行う.産業界由来のモデルによる実験により,提案手法の性能と有用性を確認するとともに,基本手法・実装については正しさの形式的検証を実施した.
|
研究成果の学術的意義や社会的意義 |
学術的意義として,一般的には扱うのが難しい大規模複雑なハイブリッドシステムを解析する手法の開発に取り組み,その効果を示す実験結果を得たことが挙げられる.有用な実例を検査するため,制約への符号化法,部品や繰り返しを考慮した検査法,モンテカルロ法との連携,大規模並列化,提案手法の実装技術等,複数の面について研究した.また,手法・実装自体の検証に取り組み,形式手法の研究過程の機械化・高信頼化を進めた意義がある. 社会的意義として,提案手法を実世界で稼働するシステムに対して適用し,そのモデルの安全性検査等に役立てられることが挙げられる.
|