2020 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 | 代数仕様 / 実時間システム / ハイブリッドシステム / 定理証明 / モデル検査 |
|---|
| Outline of Annual Research Achievements |
2020年度の各研究テーマにおける研究進捗は下記の通りです．テーマ(1) 定理証明技術とモデル検査技術を融合した形式的検証技術：定理証明技術の基礎研究として，代数仕様言語CafeOBJにおける停止性および十分完全生の証明手法を提案しました．パラメータ仕様および仕様のインポートに基づく構造的な仕様記述の際に，仕様が矛盾しないこと，および，仕様実行が有限時間内に停止することを保証する仕様記述方法を得ることができました．本研究成果を国際論文誌で発表しました[tcs]．代数仕様を用いた実時間マルチタスクシステムの仕様記述と検証方法を検討しました．2019年度に提案した仕様記述方法に基づく事例に対して，証明スコア法による検証ができることを示しました[sice1]．時間に応じて変化する物理量の記述が可能なハイブリッドシステムとして，自動運転車の加速度，速度，位置を例とした事例研究を国際会議で発表しました[sice2]．定理証明とモデル検査の融合として，CafeOBJとUPPAALのモデル間の変換技術に検討し，国内会議で発表しました[rengo]．テーマ(2) 数理最適化を用いた階層型マルチエージェントシミュレーション：高密度な都市空間における自動運転車群の最適経路探索のための数理計画について検討し，研究成果を国際会議で発表しました[sice3]．
|
| 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を用いた実時間システムおよびハイブリッドシステムの仕様記述と検証方法を定式化します．それらの手法を自動運転車群の制御アルゴリズムの設計検証に適用します. 代数仕様言語CafeOBJ, Maude，および，実時間検証ツールUPPAALの関係を整理し，それらの融合によるモデル化，検証手法を検討します．テーマ(2) 数理最適化を用いた階層型マルチエージェントシミュレーション，および，テーマ(3) 異なる手法，異なる抽象レベルの間のモデル変換理論の構築：(2)の数理最適化技術に基づく自明でない規模の事例研究に対して形式手法技術の適用を試み，事例研究を通して，両技術の融合を検討します．また，異なるモデル間の変換手法，ツールの開発を試みます.
|
| Causes of Carryover |
新型コロナの影響で研究発表および共同研究にともなう旅費の支出が予定を大幅に下回ったため
|
