形式手法と数理最適化による高信頼かつ高効率な自動運転車群制御システムの構築

使用形式化方法和数学优化构建高度可靠且高效的自动驾驶车队控制系统

• 批准号: 19K11842
• 负责人: 中村 正樹
• 金额: $ 2.75万
• 依托单位: Toyama Prefectural University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2019
• 资助国家: 日本
• 起止时间: 2019-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-19K11842/
• 关键词: ハイブリッドシステム; 実時間システム; 統計的モデル検査; 定理証明; OTS/CafeOBJ法; UPPAAL; CafeOBJ; SUMO; 自動運転車; 確率システム; モデル検査; Maude; 代数仕様; 自動運転車群制御; マルチエージェントシミュレーション; 形式手法; 数理最適化; 移動体; 群制御

2022年度の各研究テーマにおける研究進捗は下記の通りです．テーマ(1) 定理証明技術とモデル検査技術を融合した形式的検証技術およびテーマ(3) 異なる手法・抽象レベルの間のモデル変換理論の構築：代数仕様言語CafeOBJに基づく定理証明，代数仕様言語MaudeおよびUPPAALシステムに基づくモデル検査を中心に，自動運転車に関連するシステムのモデル化および検証を進めました．自動運転車の交差点制御プロトコルについて，代数仕様に基づく実時間システムの振舞仕様記述と定理証明による検証に関する研究成果を論文誌に発表しました[SEKE]．その他に，自動運転車を対象としたハイブリッドシステムの検証に関する検討を国内会議で発表しました[ISCIE]．テーマ(2) 数理最適化を用いた階層型マルチエージェントシミュレーション：SUMOを用いた自動運転車の客配送問題のシミュレータによる分析に関する研究成果を国内会議で発表しました[ISCIE,SSI]．自動運転車制御システムのモデル化および検証の前段階として，マルチカーエレベータの運行則のUAAPPLシステムによるモデル化および検証に関する研究成果を国際会議および国内会議で発表しました[ICMLC]．各テーマについて，前年度に引き続き順調に研究成果を得ており，関連する論文誌，国際会議，国内会議で発表しました．今年度の研究成果には含まれませんが，特にテーマ(3)のモデル間の変換についても検討を進めており，2023年度の発表を目指して準備を進めています．

2022年各研究主题的研究进展如下。主题（1）定理证明技术和模型检验技术相结合的形式验证技术和主题（3）不同方法和抽象层次之间的模型转换理论构建：基于代数规范语言CafeOBJ、代数规范语言Maude的定理证明我们进行了建模自动驾驶汽车相关系统的验证，重点是基于UPPAAL和UPPAAL系统的模型测试。关于自动驾驶汽车的交叉口控制协议，我们在期刊[SEKE]上发表了我们的研究成果，该研究成果涉及基于代数规范的实时系统的行为规范描述和使用定理证明的验证。此外，我们在国内会议[ISCIE]上提出了自动驾驶汽车混合动力系统验证的研究。主题（2）使用数学优化的分层多智能体仿真：我们在国内一次会议上展示了我们的研究成果，内容是使用 SUMO [ISCIE，SSI] 基于模拟器分析自动驾驶汽车乘客运送问题。作为自动驾驶车辆控制系统建模和验证的第一步，我们在国际和国内会议 [ICMLC] 上展示了使用 UAPPL 系统进行多轿厢电梯操作规则建模和验证的研究成果。延续上年的脚步，我们不断取得各主题的研究成果，并在相关期刊、国际会议、国内会议上进行展示。虽然没有包含在今年的研究成果中，但我们目前正在考虑模型之间的转换，特别是主题（3），并正在为2023年的发表做准备。

项目成果

A Simulation Model for Decentralized Control of Autonomous Vehicles in High-dencity Areas

高密度地区自动驾驶汽车分散控制仿真模型

• 发表时间: 2019
• 作者: T. Sugiyama;K. Sakakibara;M. Nakamura and H. Tamaki
• 通讯作者: M. Nakamura and H. Tamaki

自動運転車群運行の全体最適化のための機械学習を用いたモデル予測制御

使用机器学习进行模型预测控制，以实现自动驾驶车队运营的整体优化

• 发表时间: 2022
• 作者: 吉田暉;松﨑仁平;榊原一紀;中村正樹
• 通讯作者: 中村正樹

OTS/CafeOBJ法によるLim-Jeong-Park-Lee交差点制御プロトコルの形式的検証

使用 OTS/CafeOBJ 方法形式化验证 Lim-Jeong-Park-Lee 交叉口控制协议

• 发表时间: 2021
• 作者: 五十嵐竜也;中村正樹;榊原一紀
• 通讯作者: 榊原一紀

Modeling an Autonomous Vehicle Group Control System as Hybrid Automata and its Specification and Verification in Rewriting Logic

将自动驾驶车辆群控制系统建模为混合自动机及其重写逻辑的规范和验证

• 发表时间: 2021
• 作者: Yifan Wang;Masaki Nakamura;Kazutoshi Sakakibara
• 通讯作者: Kazutoshi Sakakibara

自動運転システムのSimulinkによるモデル化とSpaceExによる形式的検証

使用 Simulink 对自动驾驶系统进行建模并使用 SpaceEx 进行形式验证

• 发表时间: 2022
• 作者: 甲斐雅也;中村正樹;榊原一紀
• 通讯作者: 榊原一紀