論文の概要: 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が従来の静的解析で検出できる数よりも少ないことを示す実験を行い,その事実をアルゴリズムが特定できることを実証した。 このアルゴリズムによって提供される情報は,制御ソフトウェアのコンパイル中にレジスタ割り当てを行う間,コンパイラにとって有効であることが証明できる。 これにより、コントローラチップのコストが大幅に削減される可能性がある。

関連論文リスト

• 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)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  本稿では,専門家によるデモンストレーションの部分的な観察から,安全な出力フィードバック制御法を考察する。 まず,安全性を保証する手段として,ロバスト出力制御バリア関数(ROCBF)を提案する。 次に、安全なシステム動作を示す専門家による実証からROCBFを学習するための最適化問題を定式化する。
  論文  参考訳（メタデータ） (2021-11-18T23:21:00Z)

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

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