• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 19K11842
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 60020:Mathematical informatics-related
Research InstitutionToyama Prefectural University

Principal Investigator

中村 正樹  富山県立大学, 工学部, 教授 (40345658)

Project Period (FY) 2019-04-01 – 2025-03-31
Project Status Granted (Fiscal Year 2023)
Budget Amount *help
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2023: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2022: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2021: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2019: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Keywords定理証明 / モデル検査 / シミュレーション / ハイブリッドシステム / 実時間システム / 統計的モデル検査 / OTS/CafeOBJ法 / UPPAAL / CafeOBJ / SUMO / 自動運転車 / 確率システム / Maude / 代数仕様 / 自動運転車群制御 / マルチエージェントシミュレーション / 形式手法 / 数理最適化 / 移動体 / 群制御
Outline of Research at the Start

国内外において自動運転技術の確立に向けた実証実験が進んでおり,都市全体で集中管理された自動運転車で交通が制御されるスマートシティの近い将来の実現が期待されます.こうした将来像に向け,安全・安心なスマートシティの実現のためには,自動運転車の群制御システムを安全かつ効率的に実現するための基盤技術の確立が課題となります.本研究では,ソフトウェア工学においてシステムの離散ダイナミクスの形式的検証で有効性が確かめられている形式手法技術と制御分野の連続ダイナミクスにおける最適解導出に有効な数理最適化技術を融合し,自動運転車の群制御システムの安全性検証および最適アルゴリズム導出のための枠組みを構築します.

Outline of Annual Research Achievements

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

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

各テーマについて順調に研究成果を得ています.

Strategy for Future Research Activity

引き続き,各テーマについて研究を進めるとともに,特に代数仕様に基づく検証プラットフォームについて研究成果をまとめて,論文誌への投稿を目指します.

Report

(5 results)
  • 2023 Research-status Report
  • 2022 Research-status Report
  • 2021 Research-status Report
  • 2020 Research-status Report
  • 2019 Research-status Report
  • Research Products

    (29 results)

All 2023 2022 2021 2020 2019

All Journal Article (3 results) (of which Int'l Joint Research: 1 results,  Peer Reviewed: 3 results,  Open Access: 2 results) Presentation (26 results) (of which Int'l Joint Research: 16 results,  Invited: 1 results)

  • [Journal Article] Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method2022

    • Author(s)
      NAKAMURA Masaki、HIGASHI Shuki、SAKAKIBARA Kazutoshi、OGATA Kazuhiro
    • Journal Title

      IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

      Volume: E105.A Issue: 5 Pages: 823-832

    • DOI

      10.1587/transfun.2021MAP0007

    • NAID

      130008091333

    • ISSN
      0916-8508, 1745-1337
    • Year and Date
      2022-05-01
    • Related Report
      2022 Research-status Report 2021 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Formal Verification of Multitask Hybrid Systems by the OTS/CafeOBJ Method2021

    • Author(s)
      Nakamura Masaki、Sakakibara Kazutoshi、Okura Yuki、Ogata Kazuhiro
    • Journal Title

      International Journal of Software Engineering and Knowledge Engineering

      Volume: 31 Issue: 11n12 Pages: 1541-1559

    • DOI

      10.1142/s0218194021400118

    • Related Report
      2021 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Stability of termination and sufficient-completeness under pushouts via amalgamation2020

    • Author(s)
      Gaina Daniel、Nakamura Masaki、Ogata Kazuhiro、Futatsugi Kokichi
    • Journal Title

      Theoretical Computer Science

      Volume: 848 Pages: 82-105

    • DOI

      10.1016/j.tcs.2020.09.024

    • Related Report
      2020 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] Formal Specification and Verification of an Autonomous Vehicle Control System by the OTS/CafeOBJ method2023

    • Author(s)
      Yifan Wang, Masaki Nakamura, Kazutoshi Sakakibara, Yuki Okura
    • Organizer
      The Thirty Fifth International Conference on Software Engineering and Knowledge Engineering (SEKE 2023)
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Formal verification of an autonomous vehicle control system by the timed OTS/CafeOBJ method2023

    • Author(s)
      Yifan Wang, Masaki Nakamura, Kazutoshi Sakakibara
    • Organizer
      The 29th Int'l Conf on Parallel and Distributed Processing Techniques and Applications: Workshop on Mathematical Modeling and Problem Solving (PDPTA'23, MPS144)
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Formal verification of an autonomous vehicle control system by the timed OTS/CafeOBJ method2023

    • Author(s)
      Masaki Nakamura, Tatsuya Igarashi, Yifan Wang, Kazutoshi Sakakibara
    • Organizer
      The 29th Int'l Conf on Parallel and Distributed Processing Techniques and Applications: Workshop on Mathematical Modeling and Problem Solving (PDPTA'23, MPS144)
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Formal verification of multi-car elevator systems using statistical model checking2023

    • Author(s)
      Yuki Kitahara, Masaki Nakamura and Kazutoshi Sakakibara
    • Organizer
      The 38th International Technical Conference on Circuits/Systems, Computers, and Communications (ITC-CSCC)
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Investigation of Formal Verification of the Autonomous Vehicle Control System by Specification Translation2023

    • Author(s)
      Yifan Wang, Masaki Nakamura and Kazutoshi Sakakibara
    • Organizer
      The 38th International Technical Conference on Circuits/Systems, Computers, and Communications (ITC-CSCC)
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research
  • [Presentation] Formal Verification of the Lim-Jeong-Park-Lee Autonomous Vehicle Control Protocol using the OTS/CafeOBJ Method2022

    • Author(s)
      Igarashi Tatsuya、Nakamura Masaki、Sakakibara Kazutoshi
    • Organizer
      The Thirty Fourth International Conference on Software Engineering and Knowledge Engineering (SEKE 2022), pp.574-579, July 1-10, 2022
    • Related Report
      2022 Research-status Report
    • Int'l Joint Research
  • [Presentation] An investigation of formal verification of control policy of multi-car elevator systems using statistical model checking2022

    • Author(s)
      Yuki Kitahara, Masaki Nakamura, Kazutoshi Sakakibara
    • Organizer
      The Proceedings of the International Conference on Machine Learning and Cybernetics (ICMLC) , 6010, Toyama, 9-11 Sep. 2022
    • Related Report
      2022 Research-status Report
    • Int'l Joint Research
  • [Presentation] 到達可能性解析と定理証明を用いたハイブリッドシステムの形式的検証の検討2022

    • Author(s)
      浅井智也, 中村正樹, 榊原一紀
    • Organizer
      第66回システム制御情報学会研究発表講演会, Proceedings of the 66th annual Conference of the Institute of Systems, Control and Information Engineering (ISCIE), 321-3, pp.801-806, 2022.5.18-20
    • Related Report
      2022 Research-status Report
  • [Presentation] 自動運転システムのSimulinkによるモデル化とSpaceExによる形式的検証2022

    • Author(s)
      甲斐雅也, 中村正樹, 榊原一紀
    • Organizer
      第66回システム制御情報学会研究発表講演会, Proceedings of the 66th annual Conference of the Institute of Systems, Control and Information Engineering (ISCIE), 321-4, pp.807-813, 2022.5.18-20
    • Related Report
      2022 Research-status Report
  • [Presentation] 自動運転車群運行の全体最適化のための機械学習を用いたモデル予測制御2022

    • Author(s)
      吉田暉, 松﨑仁平, 榊原一紀, 中村正樹
    • Organizer
      第66回システム制御情報学会研究発表講演会, Proceedings of the 66th annual Conference of the Institute of Systems, Control and Information Engineering (ISCIE), 342-5, pp.1032-1039, 2022.5.18-20
    • Related Report
      2022 Research-status Report
  • [Presentation] 機械学習を用いたモデル予測制御による自動運転車群運行の全体最適化2022

    • Author(s)
      吉田暉,松崎仁平,榊原一紀,中村正樹
    • Organizer
      計測自動制御学会 システム・情報部門学術講演会2022,SS04-06,pp.377-382,2022年11月25-27日
    • Related Report
      2022 Research-status Report
  • [Presentation] 統計的モデル検査を用いたマルチカーエレベータシステムの設計検証2022

    • Author(s)
      北原祐希,中村正樹,榊原一紀
    • Organizer
      計測自動制御学会 システム・情報部門学術講演会2022,SS04-12,pp.397-402,2022年11月25-27日
    • Related Report
      2022 Research-status Report
  • [Presentation] 統計的モデル検査を用いたエレベータ制御則の設計検証の検討2022

    • Author(s)
      北原祐希,中村正樹,榊原一紀
    • Organizer
      電子情報通信学会システム数理と応用研究会
    • Related Report
      2021 Research-status Report
  • [Presentation] Modeling an Autonomous Vehicle Group Control System as Hybrid Automata and its Specification and Verification in Rewriting Logic2021

    • Author(s)
      Yifan Wang, Masaki Nakamura, Kazutoshi Sakakibara
    • Organizer
      The 36th International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2021)
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] Formal verification of multitask hybrid systems by the OTS/CafeOBJ method2021

    • Author(s)
      M. Nakamura, K. Sakakibara, Y. Okura, K. Ogata
    • Organizer
      The Thirty Third International Conference on Software Engineering and Knowledge Engineering (SEKE 2021)
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research
  • [Presentation] 形式手法の社会システムへの応用に向けた取り組み2021

    • Author(s)
      中村正樹
    • Organizer
      第65回システム制御情報学会研究発表講演会(Proceeding of the 65th Annual Conference of the Institute of Systems, Control and Information Engineers (ISCIE))
    • Related Report
      2021 Research-status Report
    • Invited
  • [Presentation] 自動運転車群運行の全体最適化2021

    • Author(s)
      吉田暉, 松﨑仁平, 榊原一紀, 中村正樹
    • Organizer
      計測自動制御学会 システム・情報部門学術講演会2021
    • Related Report
      2021 Research-status Report
  • [Presentation] OTS/CafeOBJ法によるLim-Jeong-Park-Lee交差点制御プロトコルの形式的検証2021

    • Author(s)
      五十嵐竜也, 中村正樹, 榊原一紀
    • Organizer
      計測自動制御学会 システム・情報部門学術講演会2021
    • Related Report
      2021 Research-status Report
  • [Presentation] Formal verification of Fischer’s real-time mutual exclusion protocol by the OTS/CafeOBJ method2020

    • Author(s)
      Nakamura Masaki、Higashi Shuki、Sakakibara Kazutoshi、Ogata Kazuhiro
    • Organizer
      2020 59th Annual Conference of the Society of Instrument and Control Engineers of Japan (SICE)
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] Investigation of formal specification and verification for autonomous vehicles based on rewriting logic2020

    • Author(s)
      Y. Wang, M. Nakamura, K. Sakakibara,
    • Organizer
      2020 59th Annual Conference of the Society of Instrument and Control Engineers of Japan (SICE)
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] A Mathematical Programming Model for Operational Planning of Autonomous Vehicles in High-Density Areas2020

    • Author(s)
      T. Sugiyama, K. Sakakibara, M. Nakamura, T. Inamoto, and H. Tamaki
    • Organizer
      2020 59th Annual Conference of the Society of Instrument and Control Engineers of Japan (SICE)
    • Related Report
      2020 Research-status Report
    • Int'l Joint Research
  • [Presentation] A preliminary study on specification translation from timed OTS/CafeOBJ specifications to UPPAAL specifications2020

    • Author(s)
      中村正樹
    • Organizer
      第63回自動制御連合講演会
    • Related Report
      2020 Research-status Report
  • [Presentation] Modeling and Verification of Autonomous Vehicle Group Control Algorithms2019

    • Author(s)
      M. Nakamura, Y. Sahara, C. Kojima, K. Sakakibara and H. Tamaki
    • Organizer
      Proceedings of the SICE Annual Conference 2019 (SICE 2019)
    • Related Report
      2019 Research-status Report
    • Int'l Joint Research
  • [Presentation] Formal specification of multitask real-time systems using the OTS/CafeOBJ method2019

    • Author(s)
      S. Higashi, M. Nakamura, K. Sakakibara, C. Kojima and K. Ogata
    • Organizer
      Proceedings of the SICE Annual Conference 2019 (SICE 2019)
    • Related Report
      2019 Research-status Report
    • Int'l Joint Research
  • [Presentation] A Simulation Model for Decentralized Control of Autonomous Vehicles in High-dencity Areas2019

    • Author(s)
      T. Sugiyama, K. Sakakibara, M. Nakamura and H. Tamaki
    • Organizer
      Proceedings of the SICE Annual Conference 2019 (SICE 2019)
    • Related Report
      2019 Research-status Report
    • Int'l Joint Research
  • [Presentation] Formal verification and mathematical optimization for autonomous vehicle group controllers2019

    • Author(s)
      M. Nakamura and K. Sakakibara
    • Organizer
      Proceedings of 2019 ACM/IEEE 22nd International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C)
    • Related Report
      2019 Research-status Report
    • Int'l Joint Research

URL: 

Published: 2019-04-18   Modified: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi