2019 Fiscal Year Research-status Report
形式手法と数理最適化による高信頼かつ高効率な自動運転車群制御システムの構築
| Project/Area Number |
19K11842
|
|---|
| Research Institution | Toyama Prefectural University |
|---|
Principal Investigator |
中村 正樹 富山県立大学, 工学部, 准教授 (40345658)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Keywords | 自動運転車群制御 / 定理証明 / モデル検査 / 実時間システム / マルチエージェントシミュレーション / CafeOBJ / UPPAAL |
|---|
| Outline of Annual Research Achievements |
国内外において自動運転技術の確立に向けた実証実験が進んでおり，またサイバーフィジカルシステム(CPS)やモノのインターネット(IoT)技術の発展にともない，都市全体で集中管理された自動運転車で交通が制御されるスマートシティの近い将来の実現が期待されます.こうした将来像に向け，安全・安心なスマートシティの実現のためには，信頼性が高く効率的な自動運転車の群制御システムを実現するための基盤技術の確立が課題となります.本研究では，ソフトウェア工学においてシステムの離散ダイナミクスの形式的検証で有効性が確かめられている形式手法技術と制御分野の連続ダイナミクスにおける最適解導出に有効な数理最適化技術を融合し，自動運転車の群制御システムの形式的検証と最適アルゴリズム導出のための枠組みを構築します.
2019年度の各研究テーマにおける研究進捗は下記の通りです．テーマ1. 定理証明技術とモデル検査技術を融合した形式的検証技術：定理証明技術については，基礎研究として，代数仕様言語CafeOBJを用いた実時間マルチタスクシステムの仕様記述と検証方法を提案し，国際会議発表1件，国内研究会発表1件の発表を行いました．モデル検査技術については，UPPAALツールを用いた自動運転車群の交差点制御アルゴリズムのモデル化と検証を確かめ，国際会議発表1件，国内研究会発表2件の発表を行いました．テーマ2. 数理最適化を用いた階層型マルチエージェントシミュレーション：高密度な都市空間における自動運転車群の最適経路探索のための数理計画を作成し，国際会議発表1件の発表を行いました．テーマ3. 異なる手法，異なる抽象レベルの間のモデル変換理論の構築：最適化と形式検証を用いた高効率かつ高信頼な自動運転車群の設計検証について，改めてその全体像を整理し，国際会議発表1件，国内研究会発表1件の発表を行いました．
|
| 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 |
研究実施計画に基づき，今後は各研究テーマにおいて下記のように推進します．
テーマ1. 定理証明技術とモデル検査技術を融合した形式的検証技術；代数仕様言語CafeOBJを用いた実時間マルチタスクシステムの仕様記述と検証方法を，自動運転車群の制御アルゴリズムの設計検証に適用します．
UPPAALツールによる検証対象を広げるとともに，Maudeツールによる書き換え論理に基づく設計検証を検討します．
テーマ2. 数理最適化を用いた階層型マルチエージェントシミュレーション：高密度な都市空間における自動運転車群の最適経路探索のための数理計画で作成したモデルに対し，安全性等の形式検証技術の適用を試みます．
テーマ3. 異なる手法，異なる抽象レベルの間のモデル変換理論の構築：定理証明技術とモデル検査技術の融合のために，CafeOBJ, UPPAAL, Maudeの各モデル間の変換手法，ツールの開発を試みます．
|
| Causes of Carryover |
計画していた研究調査，発表のための旅費が新型コロナの影響で中止になったため
|
