論文の概要: Implementation of the Collision Avoidance System for DO-178C Compliance

• arxiv url: http://arxiv.org/abs/2509.16844v1
• Date: Sat, 20 Sep 2025 23:52:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-30 15:01:34.640656
• Title: Implementation of the Collision Avoidance System for DO-178C Compliance
• Title（参考訳）: DO-178Cコンプライアンスのための衝突回避システムの実装
• Authors: Rim Zrelli, Henrique Amaral Misson, Sorelle Kamkuimo, Maroua Ben Attia, Abdo Shabah, Felipe Gohring de Magalhaes, Gabriela Nicolescu,
• Abstract要約: CASは、リアルタイムで衝突の脅威を自律的に検出し、評価し、回避するように設計されている。 要求仕様と検証、アーキテクチャと詳細な設計、コーディング、検証、トレーサビリティ。 統合フェーズは完全には実装されなかったが、このアプローチはUAVセーフティクリティカルシステムの認証問題に対処する上で有効であることが証明された。
• 参考スコア（独自算出の注目度）: 0.02345344155381704
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This technical report presents the detailed implementation of a Collision Avoidance System (CAS) for Unmanned Aerial Vehicles (UAVs), developed as a case study to demonstrate a rigorous methodology for achieving DO-178C compliance in safety-critical software. The CAS is based on functional requirements inspired by NASA's Access 5 project and is designed to autonomously detect, evaluate, and avoid potential collision threats in real-time, supporting the safe integration of UAVs into civil airspace. The implementation environment combines formal methods, model-based development, and automated verification tools, including Alloy, SPIN, Simulink Embedded Coder, and the LDRA tool suite. The report documents each phase of the software lifecycle: requirements specification and validation, architectural and detailed design, coding, verification, and traceability, with a strong focus on compliance with DO-178C Design Assurance Level B objectives. Results demonstrate that formal modelling and automated toolchains enabled early detection and correction of specification defects, robust traceability, and strong evidence of verification and validation across all development stages. Static and dynamic analyses confirmed code quality and coverage, while formal verification methods provided mathematical assurance of correctness for critical components. Although the integration phase was not fully implemented, the approach proved effective in addressing certification challenges for UAV safety-critical systems. \keywords Collision Avoidance System (CAS), Unmanned Aerial Vehicles (UAVs), DO-178C compliance, Safety-critical software, Formal methods, Model-based development, Alloy, SPIN model checker, Simulink Embedded Coder, LDRA tool suite, Software verification and validation, Traceability, Certification.
• Abstract（参考訳）: 本技術報告では、安全クリティカルなソフトウェアにおけるDO-178Cコンプライアンスを実現するための厳密な方法論を実証するために開発された無人航空機(UAV)の衝突回避システム(CAS)の詳細な実装について述べる。 CASはNASAのAccess 5プロジェクトから着想を得た機能要件に基づいており、UAVの民間空域への安全な統合をサポートするために、リアルタイムで衝突の脅威を自律的に検出し、評価し、回避するように設計されている。 実装環境は形式的手法、モデルベース開発、アロイ、SPIN、Simulink Embedded Coder、LDRAツールスイートなど自動検証ツールを組み合わせている。 要件仕様と検証,アーキテクチャと詳細な設計,コーディング,検証,トレーサビリティといったソフトウェアライフサイクルの各フェーズについて,DO-178C 設計保証レベル B の目標への準拠を強く重視している。 その結果、フォーマルなモデリングと自動ツールチェーンにより、仕様欠陥の早期検出と修正、堅牢なトレーサビリティ、すべての開発段階における検証と検証の強力な証拠が実現された。 静的および動的解析はコードの品質とカバレッジを確認し、形式的検証手法は臨界成分の正しさを数学的に保証した。 統合フェーズは完全には実装されなかったが、このアプローチはUAVセーフティクリティカルシステムの認証問題に対処する上で有効であることが証明された。 \keywords Collision Avoidance System (CAS)、Unmanned Aerial Vehicles (UAV)、DO-178Cコンプライアンス、セーフティクリティカルソフトウェア、フォーマルメソッド、モデルベース開発、アロイ、SPINモデルチェッカー、Simulink Embedded Coder、LDRAツールスイート、ソフトウェア検証と検証、トレーサビリティ、認証。

関連論文リスト

• Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models [0.0]
  本稿では,Slither-based detectors, Large Language Models (LLMs), Kontrol, Forgeを統合した新しい検出パイプラインを提案する。 私たちのアプローチは、欠陥を確実に検出し、証明を生成するように設計されています。
  論文  参考訳（メタデータ） (2025-09-16T12:46:11Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• An Automated Blackbox Noncompliance Checker for QUIC Server Implementations [2.9248916859490173]
  QUICtesterは、承認されたQUICプロトコル実装(RFC 9000/)における非準拠の動作を明らかにするための自動化アプローチである。 我々はQUICtesterを用いて、19のQUIC実装から得られた186個の学習モデルを5つのセキュリティ設定で解析し、55個の実装エラーを発見した。
  論文  参考訳（メタデータ） (2025-05-19T04:28:49Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。 問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。 本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
  論文  参考訳（メタデータ） (2024-03-15T17:32:02Z)
• Simulation-based Safety Assurance for an AVP System incorporating Learning-Enabled Components [0.6526824510982802]
  テスト、検証、検証 AD/ADASセーフティクリティカルなアプリケーションが大きな課題のひとつとして残っています。 安全クリティカルな学習可能システムの検証と検証を目的としたシミュレーションベースの開発プラットフォームについて説明する。
  論文  参考訳（メタデータ） (2023-09-28T09:00:31Z)
• 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)
• A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems [30.638615396429536]
  安全クリティカルな人工知能の普及により、この研究は、CPSの最先端の安全検証技術の調査を提供する。 本稿では,最適化,経路計画,強化学習,重要サンプリングの分野におけるアルゴリズムについて論じる。 自動運転車や航空機衝突回避システムなど、安全クリティカルな応用の概要を概説する。
  論文  参考訳（メタデータ） (2020-05-06T17:31:51Z)

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

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