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

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

• 批准号: 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的定理证明，以及基于Algebraic Speceification Languepiencation Language and uppa Maude Maude Maude and Uppa audpa and uppa audpa and uppa audpa and uppa audpa and uppa audpa system。我们已经在《自动驾驶车辆的交叉路口控制方案》的行为规范中发表了研究结果，并使用基于代数规格的实时系统的行为证明[SEKE]进行了验证。此外，在国内会议[ISCIE]上宣布了对自动驾驶汽车混合动力系统验证的审查。主题（2）使用数学优化的分层多代理模拟：在国内会议[ISCIE，SSI]上介绍了使用SUMO使用SUMO在自动驾驶汽车中分析客户交付问题的研究结果。作为建模和验证自动驾驶汽车控制系统的初步阶段，在国际和国内会议[ICMLC]上介绍了有关使用UAAPPL系统建模和验证多车电梯操作规则的研究结果。每个主题的研究结果都像上一年一样稳步增长，并在相关期刊，国际会议和国内会议上提出。尽管这不包括在今年的研究结果中，但我们也在考虑主题（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
• 作者: 甲斐雅也;中村正樹;榊原一紀
• 通讯作者: 榊原一紀