論文の概要: Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring

• arxiv url: http://arxiv.org/abs/2610.15418v1
• Date: Sun, 11 Oct 2026 07:44:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-20 01:16:22.581779
• Title: Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring
• Title（参考訳）: モデル検証と実行監視を組み合わせた自動ウェアコントローラノードの検証
• Abstract要約: ディファレンシャル・ダイナミック・ロジック(dL)におけるハイブリッド・システムとしてコントローラを形式化する。 次に、KeYmaera X証明アシスタントを用いてモデルの安全性と生存性を証明した。 実験の結果, (i) 監視は, 精度境界の追従対象の音響評価を提供し, (ii) オートウェアの実装は, 約0.2-0.4m, 0.8m/sの精度で目標に達することを確認した。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal modeling and verification of autonomous driving systems remain challenging due to the vast operational space and the complexity of the control logic. We propose a hybrid verification approach that combines formal model verification and runtime monitoring for the trajectory-following control node of Autoware, an open-source autonomous driving platform. We formalize the controller as a hybrid system in differential dynamic logic (dL), and introduce an abstract model that captures the essential control dynamics. We then prove safety and liveness properties of the model using the KeYmaera X proof assistant. Complementarily, we monitor the constraints that assure the compatibility between the model and the Autoware implementation across numerical simulation runs using the Autoware toolchain, quantifying to what extent the implementation's behavior is subsumed by the verified model. The experimental results confirmed that (i) monitoring provides a sound evaluation of target following with accuracy bounds, and (ii) the Autoware implementation reaches the target with an accuracy of approximately 0.2-0.4 (m) in position and 0.8 (m/s) in velocity.
• Abstract（参考訳）: 自律運転システムの形式的モデリングと検証は、膨大な運用空間と制御論理の複雑さのために依然として困難である。 本稿では,オープンソースの自動運転プラットフォームであるAutowareの軌道追従制御ノードに対して,形式的モデル検証とランタイム監視を組み合わせたハイブリッド検証手法を提案する。 差動力学(dL)におけるハイブリッドシステムとしてコントローラを形式化し,本質的な制御力学を捉える抽象モデルを導入する。 次に、KeYmaera X証明アシスタントを用いてモデルの安全性と生存性を証明した。 相補的に、数値シミュレーションにおけるモデルとAutoware実装の互換性を保証する制約を、Autowareツールチェーンを使用して監視し、検証されたモデルによって実装の振る舞いがどの程度仮定されるかを定量化する。 実験の結果、 二 監視により、精度境界の追従対象の音質評価を行い、 (i)オートウェアの実装は、位置が0.2-0.4(m)、速度が0.8(m/s)の精度で目標に達する。

関連論文リスト

• LLA-MPC on Embedded Hardware: Rapid Adaptive Control with Thousands of Parallel Models [16.266017092260153]
  LLA-MPCはリアルタイム適応型システム識別と制御のための学習自由フレームワークである。 システムは、組込みコンピュータ上で数千の候補モデルをリアルタイムで評価することで、タイヤパラメータをオンラインで識別する。 LLA-MPCは、固定された名目モデルが失敗する高速なタスクを完了することを示す。
  論文  参考訳（メタデータ） (2026-10-02T17:13:34Z)
• CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
  我々は、フロンティアモデル全体でのtextbfcontrol textbfintervention (CI) の認識を測定するベンチマークである textbfCIAware-Bench を紹介する。 CIAware-Benchは、モデルが自身の軌跡を制御介入によって修正されたものと区別できるかどうかをテストする。
  論文  参考訳（メタデータ） (2026-06-09T16:24:16Z)
• Analyzing the Impact of Simulation Fidelity on the Evaluation of Autonomous Driving Motion Control [4.815503491342169]
  総合的なAutoware互換車モデルを導入する。 我々は,各モデルの近似品質を定量化するために,550回以上のシミュレーション実行を評価した。 我々は、制御アルゴリズムを評価するために、車両モデルをどの程度単純化できるかを推定する。
  論文  参考訳（メタデータ） (2026-02-08T14:21:14Z)
• AutoDrive-R$^2$: Incentivizing Reasoning and Self-Reflection Capacity for VLA Model in Autonomous Driving [37.260140808367716]
  本稿では,自律運転システムの推論能力と自己回帰能力を両立させる新しいVLAフレームワークであるAutoDrive-R$2$を提案する。 まず,教師付き微調整のための新しいCoTデータセット nuScenesR$2$-6K を提案する。 次に, グループ相対政策最適化(GRPO)アルゴリズムを用いて, 信頼性の高い滑らかさと現実的な軌道計画を実現する。
  論文  参考訳（メタデータ） (2025-09-02T04:32:24Z)
• Deep Bilinear Koopman Model for Real-Time Vehicle Control in Frenet Frame [0.0]
  本稿では,カービリニアFrenetフレーム内の車両力学のモデリングと制御のための深いクープマン手法を提案する。 提案フレームワークは、深層ニューラルネットワークアーキテクチャを使用して、データからクープマン演算子とその関連する不変部分空間を同時に学習する。 提案した制御器は, ベースライン制御器と比較して追従誤差を著しく低減し, 組込み自動運転車システムにおけるリアルタイム実装に適していることを確認した。
  論文  参考訳（メタデータ） (2025-07-16T18:49:44Z)
• AgentThink: A Unified Framework for Tool-Augmented Chain-of-Thought Reasoning in Vision-Language Models for Autonomous Driving [31.127210974372456]
  VLM(Vision-Language Models)は、自律走行を約束するが、幻覚、非効率な推論、限られた実世界の検証は、正確な知覚と堅牢なステップバイステップ推論を妨げる。 我々は、Chain-of-Thought(CoT)推論と、自律運転タスクのための動的エージェントスタイルのツール呼び出しを統合した、先駆的な統合フレームワークであるtextbfAgentThinkを紹介した。
  論文  参考訳（メタデータ） (2025-05-21T09:27:43Z)
• Trajeglish: Traffic Modeling as Next-Token Prediction [67.28197954427638]
  自動運転開発における長年の課題は、記録された運転ログからシードされた動的運転シナリオをシミュレートすることだ。 車両、歩行者、サイクリストが運転シナリオでどのように相互作用するかをモデル化するために、離散シーケンスモデリングのツールを適用します。 我々のモデルはSim Agents Benchmarkを上回り、リアリズムメタメトリックの先行作業の3.3%、インタラクションメトリックの9.9%を上回ります。
  論文  参考訳（メタデータ） (2023-12-07T18:53:27Z)
• End-to-End Reinforcement Learning of Koopman Models for Economic Nonlinear Model Predictive Control [45.84205238554709]
  本研究では, (e)NMPCの一部として最適性能を示すために, Koopman シュロゲートモデルの強化学習法を提案する。 エンドツーエンドトレーニングモデルは,(e)NMPCにおけるシステム識別を用いてトレーニングしたモデルよりも優れていることを示す。
  論文  参考訳（メタデータ） (2023-08-03T10:21:53Z)
• A Driving Behavior Recognition Model with Bi-LSTM and Multi-Scale CNN [59.57221522897815]
  運転行動認識のための軌道情報に基づくニューラルネットワークモデルを提案する。 提案手法を公開BLVDデータセット上で評価し,満足な性能を実現する。
  論文  参考訳（メタデータ） (2021-03-01T06:47:29Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。