論文の概要: Towards Continuous Assurance with Formal Verification and Assurance Cases

• arxiv url: http://arxiv.org/abs/2511.14805v1
• Date: Mon, 17 Nov 2025 18:42:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-20 15:51:28.468382
• Title: Towards Continuous Assurance with Formal Verification and Assurance Cases
• Title（参考訳）: 形式的検証と保証事例による継続的保証に向けて
• Authors: Dhaminda B. Abeywickrama, Michael Fisher, Frederic Wheeler, Louise Dennis,
• Abstract要約: 我々は、トレース可能なモデル駆動ワークフロー内に設計時、実行時、進化時保証を統合する統合された継続的保証フレームワークを提案する。 我々は,核検査ロボットのシナリオに対するアプローチを実証し,三元AI原則との整合性について議論する。
• 参考スコア（独自算出の注目度）: 0.5483130283061118
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Autonomous systems must sustain justified confidence in their correctness and safety across their operational lifecycle-from design and deployment through post-deployment evolution. Traditional assurance methods often separate development-time assurance from runtime assurance, yielding fragmented arguments that cannot adapt to runtime changes or system updates - a significant challenge for assured autonomy. Towards addressing this, we propose a unified Continuous Assurance Framework that integrates design-time, runtime, and evolution-time assurance within a traceable, model-driven workflow as a step towards assured autonomy. In this paper, we specifically instantiate the design-time phase of the framework using two formal verification methods: RoboChart for functional correctness and PRISM for probabilistic risk analysis. We also propose a model-driven transformation pipeline, implemented as an Eclipse plugin, that automatically regenerates structured assurance arguments whenever formal specifications or their verification results change, thereby ensuring traceability. We demonstrate our approach on a nuclear inspection robot scenario, and discuss its alignment with the Trilateral AI Principles, reflecting regulator-endorsed best practices.
• Abstract（参考訳）: 自律システムは、デプロイ後の進化を通じて、設計とデプロイメントから運用ライフサイクル全体にわたって、その正しさと安全性に対する正当性を維持する必要があります。 従来の保証メソッドは、しばしばランタイムの保証から開発時の保証を分離し、ランタイムの変更やシステム更新に適応できない断片化された引数を生成する。 これに対応するために、我々は、自律性を保証するためのステップとして、トレース可能なモデル駆動ワークフローに設計時、実行時、進化時保証を統合する統合された継続的保証フレームワークを提案します。 本稿では,機能的正当性のためのRoboChartと確率的リスク分析のためのPRISMという2つの形式的検証手法を用いて,フレームワークの設計時フェーズを具体的にインスタンス化する。 また,Eclipseプラグインとして実装されたモデル駆動型トランスフォーメーションパイプラインを提案し,形式仕様や検証結果が変更されるたびに,構造化された保証引数を自動的に再生し,トレーサビリティを確保する。 我々は,核検査ロボットのシナリオに対するアプローチを実証し,規制に適合したベストプラクティスを反映した三元AI原則との整合性について議論する。

関連論文リスト

• A Scalable Framework for Safety Assurance of Self-Driving Vehicles based on Assurance 2.0 [3.2877342344625777]
  Assurance 2.0は、ますます複雑で適応的で自律的なシステムの保証問題に対処するために開発されたモダンなフレームワークである。 厳密さ、透明性、適応性を高めるために、再利用可能な保証理論と明示的な対抗策(デファター)を導入している。 限界は、信頼度測定、疑念の残る管理、自動化支援、そして、敗者および確認バイアスの実践的な処理に持続する。
  論文  参考訳（メタデータ） (2025-09-30T16:13:03Z)
• AgentGuard: Runtime Verification of AI Agents [1.14219428942199]
  AgentGuardは、エージェントAIシステムの実行時検証のためのフレームワークである。 動的確率保証(Dynamic Probabilistic Assurance)と呼ばれる新しいパラダイムを通じて、継続的な量的保証を提供する。
  論文  参考訳（メタデータ） (2025-09-28T13:08:50Z)
• CARE: Decoding Time Safety Alignment via Rollback and Introspection Intervention [68.95008546581339]
  Contrastive Decodingのような既存のデコーディングタイムの介入は、安全と応答品質の間に深刻なトレードオフを強いることが多い。 本稿では,3つの重要なコンポーネントを統合した,復号時安全アライメントのための新しいフレームワークであるCAREを提案する。 このフレームワークは、安全性、品質、効率のバランスが良く、有害な応答率が低く、ユーザエクスペリエンスを最小限に破壊できる。
  論文  参考訳（メタデータ） (2025-09-01T04:50:02Z)
• Trust, But Verify: A Self-Verification Approach to Reinforcement Learning with Verifiable Rewards [67.86091419220816]
  大規模言語モデル(LLM)は複雑な推論において非常に有望である。 一般的な問題は表面的な自己回帰であり、モデルが自身の出力をしっかりと検証できない。 本稿では、RISE(Reinforce Reasoning with Self-Verification)という新しいオンラインRLフレームワークについて紹介する。
  論文  参考訳（メタデータ） (2025-05-19T17:59:31Z)
• Engineering Risk-Aware, Security-by-Design Frameworks for Assurance of Large-Scale Autonomous AI Models [0.0]
  本稿では,大規模自律型AIシステムを対象とした企業レベルのリスク認識型セキュリティ・バイ・デザイン手法を提案する。 敵的および運用的ストレス下でのモデル動作の証明可能な保証を提供する統一パイプラインについて詳述する。 国家安全保障、オープンソースモデルガバナンス、産業自動化におけるケーススタディは、脆弱性とコンプライアンスのオーバーヘッドの計測可能な削減を実証している。
  論文  参考訳（メタデータ） (2025-05-09T20:14:53Z)
• Know Where You're Uncertain When Planning with Multimodal Foundation Models: A Formal Framework [54.40508478482667]
  認識と計画生成の不確実性を解消し、定量化し、緩和する包括的枠組みを提案する。 本稿では,知覚と意思決定の独特な性質に合わせた手法を提案する。 この不確実性分散フレームワークは, 変動率を最大40%削減し, タスク成功率をベースラインに比べて5%向上させることを示した。
  論文  参考訳（メタデータ） (2024-11-03T17:32:00Z)
• ACCESS: Assurance Case Centric Engineering of Safety-critical Systems [9.388301205192082]
  保証ケースは、安全性やセキュリティなどの重要なシステム特性について、コミュニケーションし、信頼性を評価するために使用されます。 近年,システム保証活動の効率化と品質向上のために,モデルに基づくシステム保証アプローチが普及している。 モデルに基づくシステム保証ケースが異種工学的アーティファクトにどのように辿り着くかを示す。
  論文  参考訳（メタデータ） (2024-03-22T14:29:50Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)

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

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