論文の概要: A Formal Verification Approach to Safeguard Controller Variables from Single Event Upset

• arxiv url: http://arxiv.org/abs/2505.06648v1
• Date: Sat, 10 May 2025 13:56:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-13 20:21:48.963367
• Title: A Formal Verification Approach to Safeguard Controller Variables from Single Event Upset
• Title（参考訳）: 単一イベントからの安全制御器変数の形式的検証手法
• Authors: Ganesha, Sujit Kumar Chakrabarti,
• Abstract要約: プログラム解析と形式検証に基づく条件付き変数(CRV)の同定手法を提案する。 CRVは、単一イベントの混乱(SEU)の影響を受け、制御ソフトウェアにおける安全性の侵害につながる可能性がある
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a method based on program analysis and formal verification to identify conditionally relevant variables (CRVs) - variables which could lead to violation of safety properties in control software when affected by single event upsets (SEUs). Traditional static analysis can distinguish between relevant and irrelevant variables. However, it would fail to take into account the conditions specific to the control software in question. This can lead to false positives. Our algorithm employs formal verification to avoid false positives. We have conducted experiments that demonstrate that CRVs indeed are fewer in number than what traditional static analysis can detect and that our algorithm is able to identify this fact. The information provided by our algorithm could prove helpful to a compiler while it does register allocation during the compilation of the control software. In turn, this could cause significant reduction in the cost of controller chips.
• Abstract（参考訳）: 本稿では,プログラム解析と形式検証に基づく条件付き変数(CRV)の同定手法を提案する。 従来の静的解析は、関連する変数と無関係変数を区別することができる。 しかし、問題のコントロールソフトウェアに特有の条件を考慮に入れなかっただろう。 これは偽陽性につながる可能性がある。 我々のアルゴリズムは偽陽性を避けるために形式的検証を用いる。 我々は,CRVが従来の静的解析で検出できる数よりも少ないことを示す実験を行い,その事実をアルゴリズムが特定できることを実証した。 このアルゴリズムによって提供される情報は,制御ソフトウェアのコンパイル中にレジスタ割り当てを行う間,コンパイラにとって有効であることが証明できる。 これにより、コントローラチップのコストが大幅に削減される可能性がある。

関連論文リスト

• CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
  物理ECUアクティベーションに基づく最初の決定論的侵入検知・防止システムであるCANTXSecを提案する。 CANバスの古典的な攻撃を検知・防止し、文献では調査されていない高度な攻撃を検知する。 物理テストベッド上での解法の有効性を実証し,攻撃の両クラスにおいて100%検出精度を達成し,100%のFIAを防止した。
  論文  参考訳（メタデータ） (2025-05-14T13:37:07Z)
• Checkification: A Practical Approach for Testing Static Analysis Truths [0.0]
  本稿では,抽象解釈に基づく静的アナライザの試験法を提案する。 このアプローチの主な利点は、Ciaoアサーションベースのバリデーションフレームワーク内で直接フレーミングすることによる、シンプルさにあります。 我々は、CiaoPP静的解析器にアプローチを適用し、合理的なオーバーヘッドを伴う多くのバグを特定した。
  論文  参考訳（メタデータ） (2025-01-21T12:38:04Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)
• Geospatial Trajectory Generation via Efficient Abduction: Deployment for Independent Testing [1.8877926393541125]
  情報(A*)探索により,移動軌跡を効率的に吸収できることが示される。 私たちはまた、正確な結果を提供するだけでなく、非常に大きなシナリオにもスケールできることを示す独自の実験について報告します。
  論文  参考訳（メタデータ） (2024-07-08T23:11:47Z)
• Automatically Adaptive Conformal Risk Control [49.95190019041905]
  本稿では,テストサンプルの難易度に適応して,統計的リスクの近似的条件制御を実現する手法を提案する。 我々のフレームワークは、ユーザが提供するコンディショニングイベントに基づく従来のコンディショニングリスク制御を超えて、コンディショニングに適した関数クラスのアルゴリズム的、データ駆動決定を行う。
  論文  参考訳（メタデータ） (2024-06-25T08:29:32Z)
• BEC: Bit-Level Static Analysis for Reliability against Soft Errors [0.26107298043931204]
  ソフトエラーに対するプログラムの信頼性を理解し改善するためのビットレベルエラー照合(BEC)静的プログラム解析を提案する。 BEC分析はレジスタファイル内の各ビットの破損を追跡し、コンパイル時にその意味によって破損の影響を分類する。 提案手法は汎用的であり,特定のコンピュータアーキテクチャに限定されない。
  論文  参考訳（メタデータ） (2024-01-11T09:03:47Z)
• Conformal Policy Learning for Sensorimotor Control Under Distribution Shifts [61.929388479847525]
  本稿では,センサコントローラの観測値の分布変化を検知・応答する問題に焦点をあてる。 鍵となる考え方は、整合量子を入力として取ることができるスイッチングポリシーの設計である。 本稿では, 基本方針を異なる特性で切り替えるために, 共形量子関数を用いてこのようなポリシーを設計する方法を示す。
  論文  参考訳（メタデータ） (2023-11-02T17:59:30Z)
• Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version) [1.3749490831384268]
  情報を意図的に漏洩する非自明な並行プログラムのセキュリティを特定・証明する問題を考察する。 本稿では,この問題を (a) 帰納的プログラム検証ですでに広く使用されているアノテーションを前提として,プログラムが情報のみを漏らすことを証明した手法を提案する。 また,既存のプログラム論理 SecCSL の拡張によって条件 (a) がどのように強制されるか,そして (b) が簡単な内容の集合を証明してどのようにチェックできるかを示す。
  論文  参考訳（メタデータ） (2023-09-07T01:51:41Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  雑音分布の明示的な表現に依存しない新しい制御器合成法を提案する。 まず、連続制御系を有限状態モデルに抽象化し、離散状態間の確率的遷移によってノイズを捕捉する。 我々は最先端の検証技術を用いてマルコフ決定プロセスの間隔を保証し、これらの保証が元の制御システムに受け継がれるコントローラを演算する。
  論文  参考訳（メタデータ） (2023-01-04T10:40:30Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  本稿では,専門家によるデモンストレーションの部分的な観察から,安全な出力フィードバック制御法を考察する。 まず,安全性を保証する手段として,ロバスト出力制御バリア関数(ROCBF)を提案する。 次に、安全なシステム動作を示す専門家による実証からROCBFを学習するための最適化問題を定式化する。
  論文  参考訳（メタデータ） (2021-11-18T23:21:00Z)
• Learn then Test: Calibrating Predictive Algorithms to Achieve Risk Control [67.52000805944924]
  Learn then Test (LTT)は、機械学習モデルを校正するフレームワークである。 私たちの主な洞察は、リスクコントロール問題を複数の仮説テストとして再設計することです。 我々は、コンピュータビジョンの詳細な実例を用いて、コア機械学習タスクの新しいキャリブレーション手法を提供するために、我々のフレームワークを使用します。
  論文  参考訳（メタデータ） (2021-10-03T17:42:03Z)

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

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