論文の概要: Formal Evidence Generation for Assurance Cases for Robotic Software Models

• arxiv url: http://arxiv.org/abs/2602.03550v1
• Date: Tue, 03 Feb 2026 14:01:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-04 18:37:15.491784
• Title: Formal Evidence Generation for Assurance Cases for Robotic Software Models
• Title（参考訳）: ロボットソフトウェアモデルにおける保証事例の形式的エビデンス生成
• Authors: Fang Yan, Simon Foster, Ana Cavalcanti, Ibrahim Habli, James Baxter,
• Abstract要約: 保証ケースは、証拠によって支持される構造化された議論を提供する。 この証拠の生成と維持は、労働集約的で、エラーを起こし、システムが進化するにつれて一貫性を維持するのが困難である。 本稿では,保証ワークフローに形式検証を組み込むことにより,AC証拠を体系的に生成するモデルに基づく手法を提案する。
• 参考スコア（独自算出の注目度）: 1.8145248907978841
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Robotics and Autonomous Systems are increasingly deployed in safety-critical domains, so that demonstrating their safety is essential. Assurance Cases (ACs) provide structured arguments supported by evidence, but generating and maintaining this evidence is labour-intensive, error-prone, and difficult to keep consistent as systems evolve. We present a model-based approach to systematically generating AC evidence by embedding formal verification into the assurance workflow. The approach addresses three challenges: systematically deriving formal assertions from natural language requirements using templates, orchestrating multiple formal verification tools to handle diverse property types, and integrating formal evidence production into the workflow. Leveraging RoboChart, a domain-specific modelling language with formal semantics, we combine model checking and theorem proving in our approach. Structured requirements are automatically transformed into formal assertions using predefined templates, and verification results are automatically integrated as evidence. Case studies demonstrate the effectiveness of our approach.
• Abstract（参考訳）: ロボティクスと自律システム(Autonomous Systems)は、安全クリティカルな領域にますます展開され、安全性の実証が不可欠である。 保証事例(ACs)は、証拠によって支持される構造化された議論を提供するが、この証拠の生成と維持は、労働集約的で、エラーを起こし、システムが進化するにつれて一貫性を維持するのが困難である。 本稿では,保証ワークフローに形式検証を組み込むことにより,AC証拠を体系的に生成するモデルに基づく手法を提案する。 アプローチは3つの課題に対処する: テンプレートを使用して自然言語要求から形式的アサーションを体系的に導き、さまざまなプロパティタイプを扱うために複数の形式的検証ツールを編成し、形式的エビデンスをワークフローに統合する。 形式的な意味を持つドメイン固有モデリング言語であるRoboChartを利用することで、モデルチェックと定理証明を併用する。 構造化された要件は、事前に定義されたテンプレートを使用して自動的に形式的なアサーションに変換され、検証結果がエビデンスとして自動的に統合される。 ケーススタディは、我々のアプローチの有効性を示します。

関連論文リスト

• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。 これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
  論文  参考訳（メタデータ） (2025-09-28T06:32:14Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1は、このギャップを埋めるための自動化および半自動化アプローチを調査することを目的としている。 本論文では, 課題の繰り返しと今後の研究方向性を明らかにするために, 関連文献の予備的な合成について述べる。
  論文  参考訳（メタデータ） (2025-07-18T19:15:50Z)
• Justified Evidence Collection for Argument-based AI Fairness Assurance [7.65321625950609]
  本稿では,2段階の議論に基づく保証に対する動的アプローチを運用するために,ソフトウェアツールがサポートするシステムエンジニアリング駆動フレームワークを提案する。 フレームワークの有効性は、フェアネスに関連する議論を支援することに焦点を当てた、金融における実証的なケーススタディによって実証される。
  論文  参考訳（メタデータ） (2025-05-12T21:05:33Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)

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

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