| 研究課題/領域番号 |
19K11842
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60020:数理情報学関連
|
|---|
| 研究機関 | 富山県立大学 |
|---|
研究代表者 |
中村 正樹 富山県立大学, 工学部, 教授 (40345658)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2023年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2022年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2021年度: 520千円 (直接経費: 400千円、間接経費: 120千円)
2020年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2019年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | 定理証明 / モデル検査 / シミュレーション / ハイブリッドシステム / 実時間システム / 統計的モデル検査 / OTS/CafeOBJ法 / UPPAAL / CafeOBJ / SUMO / 自動運転車 / 確率システム / Maude / 代数仕様 / 自動運転車群制御 / マルチエージェントシミュレーション / 形式手法 / 数理最適化 / 移動体 / 群制御 |
|---|
| 研究開始時の研究の概要 |
国内外において自動運転技術の確立に向けた実証実験が進んでおり，都市全体で集中管理された自動運転車で交通が制御されるスマートシティの近い将来の実現が期待されます．こうした将来像に向け，安全・安心なスマートシティの実現のためには，自動運転車の群制御システムを安全かつ効率的に実現するための基盤技術の確立が課題となります．本研究では，ソフトウェア工学においてシステムの離散ダイナミクスの形式的検証で有効性が確かめられている形式手法技術と制御分野の連続ダイナミクスにおける最適解導出に有効な数理最適化技術を融合し，自動運転車の群制御システムの安全性検証および最適アルゴリズム導出のための枠組みを構築します．
|
| 研究実績の概要 |
2023年度では，各テーマについて，前年度に引き続き順調に研究成果を得ており，関連する論文誌，国際会議，国内会議で発表しました．各研究テーマにおける詳細は下記の通りです．
テーマ(1) 定理証明技術とモデル検査技術を融合した形式的検証技術およびテーマ(3) 異なる手法・抽象レベルの間のモデル変換理論の構築：
代数仕様言語 CafeOBJに基づく定理証明，代数仕様言語MaudeおよびUPPAALシステムに基づくモデル検査を中心に，自動運転車に関連するシステムのモデル化および検証を進めました．自動運転車の群制御プロトコルについて，代数仕様に基づく実時間システムの振舞仕様記述と定理証明による検証に関する研究成果を国際会議で発表しました[SEKE2023, PDPTA23]．定理証明とモデル検査の橋渡しとなる振舞仕様から書換仕様への仕様変換の自動運転仕様への適用についての研究成果を国際会議で発表しました[ITC-CSCC2023]，その他に，自動運転車を対象としたハイブリッドシステムの検証に関する検討，および，交差点制御プロトコルのシミュレーションベースの統計的モデル検査による分析手法の検討についての研究成果を国内会議で発表しました[SCI23, SSI2023].
テーマ(2) 数理最適化を用いた階層型マルチエージェントシミュレーション：
SUMOを用いた自動運転車の客配送問題のシミュレータによる分析に関する研究成果を国内会議で発表しました[SCI23, SSI2023]．自動運転車制御システムのモデル化および検証の前段階として，マルチカーエレベータの運行則のUAAPPLシステムによ るモデル化および検証に関する研究成果を国際会議で発表しました [ITC-CSCC2023]．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
各テーマについて順調に研究成果を得ています．
|
| 今後の研究の推進方策 |
引き続き，各テーマについて研究を進めるとともに，特に代数仕様に基づく検証プラットフォームについて研究成果をまとめて，論文誌への投稿を目指します．
|
