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

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

• 批准号: 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年度の発表を目指して準備を進めています．

Research progress in 2022 is recorded below. (1) Theorem proving technique and model checking technique;(3) different technique; abstract model; transformation theory; algebraic model speech; CafeOBJ theorem proving; algebraic model speech; Maude and UPPAAL model; basic model checking center; automatic vehicle; correlation model; model checking; [SEKE] is a research achievement on the intersection control of automatic transport vehicles, the description of the basic time and the proof of the theorem. Other topics include automatic transportation of vehicles, and discussion of domestic conference presentations [ISCIE]. (2) Mathematical optimization of the use of hierarchical model of the customer distribution problem of SUMO related research results were presented to the domestic conference [ISCIE,SSI]. UAAPPL system of automatic vehicle control system, the first stage of the system, the second stage of the system, the third stage of the system, the fourth stage of the system, the system, the fourth stage of the system, the system, the system, Each year, the research results of the previous year were introduced, and the relevant papers, international conferences, and domestic conferences were presented. This year's research results include the following: (3) The research results of this year include the research results of this year, especially the research results of this year's research results.

项目成果

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

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

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

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

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

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

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

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

Formal verification of Fischer’s real-time mutual exclusion protocol by the OTS/CafeOBJ method

OTS/CafeOBJ方法形式化验证Fischer实时互斥协议

• 发表时间: 2020
• 作者: Nakamura Masaki;Higashi Shuki;Sakakibara Kazutoshi;Ogata Kazuhiro
• 通讯作者: Ogata Kazuhiro