論文の概要: Relevant HAL Interface Requirements for Embedded Systems

• arxiv url: http://arxiv.org/abs/2512.14514v1
• Date: Tue, 16 Dec 2025 15:47:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-17 16:49:26.772868
• Title: Relevant HAL Interface Requirements for Embedded Systems
• Title（参考訳）: 組込みシステムにおける関連HALインタフェース要件
• Authors: Manuel Bentele, Andreas Podelski, Axel Sikora, Bernd Westphal,
• Abstract要約: ハードウェア抽象化層(HAL)の適切な使用は、システム障害につながる可能性がある。 本稿では,システム障害に関する報告から,証明可能な要件を抽出する手法を提案する。
• 参考スコア（独自算出の注目度）: 1.1199585259018456
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Embedded applications often use a Hardware Abstraction Layer (HAL) to access hardware. Improper use of the HAL can lead to incorrect hardware operations, resulting in system failure and potentially serious damage to the hardware. The question is how one can obtain prioritize, among a possibly large set of HAL interface requirements, those that are indisputably relevant for preventing this kind of system failure. In this paper, we introduce a formal notion of relevance. This allows us to leverage a formal method, i.e., software model checking, to produce a mathematical proof that a requirement is indisputably relevant. We propose an approach to extract provably relevant requirements from issue reports on system failures. We present a case study to demonstrate that the approach is feasible in principle. The case study uses three examples of issue reports on embedded applications that use the SPI bus via the spidev HAL. The overall contribution of this paper is to pave the way for the study of approaches to a new kind of prioritization aimed at preventing a specific kind of system failure.
• Abstract（参考訳）: 組み込みアプリケーションはハードウェア・抽象化・レイヤ(HAL)を使ってハードウェアにアクセスすることが多い。 HALを不適切な使用は、ハードウェア操作を誤ったものにし、システム障害とハードウェアに深刻なダメージを与える可能性がある。 問題は、どのように優先順位を付けることができるか、そして、おそらく大きなHALインターフェースの要求の中で、この種のシステム障害を防ぐのに間違いなく関係しているものについてである。 本稿では,関連性に関する公式な概念を紹介する。 これにより、ソフトウェアモデルチェックという形式的な手法を利用して、要求が不確定に関係しているという数学的証明を作成できる。 本稿では,システム障害に関する報告から,証明可能な要件を抽出する手法を提案する。 本稿では,本手法が原則として実現可能であることを示すケーススタディを提案する。 ケーススタディでは,spedev HAL経由でSPIバスを使用する組み込みアプリケーションに関するイシューレポートの3つの例を用いている。 本論文の総合的な貢献は,システム障害を防止することを目的とした,新しいタイプの優先順位付けへのアプローチの道を開くことである。

関連論文リスト

• AQER: a scalable and efficient data loader for digital quantum computers [62.40228216126285]
  我々は,ターゲット状態の絡み合いを体系的に低減し,負荷回路を構成するスケーラブルなAQL手法であるAQERを開発した。 我々は、合成データセット、古典画像および言語データセット、最大50キュービットの量子多体状態データセットを用いて、AQERの有効性を評価するための体系的な実験を行う。
  論文  参考訳（メタデータ） (2026-02-02T14:39:42Z)
• Checking the HAL Interface Specification Continuously, Right from the Start [1.0439136407307046]
  ステップ間の正式な接続なしに,複数のイテレーションで組込みアプリケーションを開発します。 このアプローチのアイデアは、ソフトウェアモデルチェックの特定の機能を活用することです。 このアプローチに従って、チェックは各ステップ、特に最終アプリケーションプログラムで成功します。
  論文  参考訳（メタデータ） (2025-12-18T18:55:17Z)
• UOOR: Seamless and Traceable Requirements [28.579389358111115]
  提案手法は,UOORと呼ばれる要求工学手法である。 このメソッドは多くの既知の要件概念を統一し、プロジェクトライフサイクル全体を通してシームレスな変更に対応およびサポートするために完全に設計されたフレームワークに新しいものをいくつか追加します。 UOORアプローチは単なる理論的な提案ではなく、実用のために設計され、重要な実世界のケーススタディであるRoboraceに応用されている。
  論文  参考訳（メタデータ） (2025-02-25T20:03:01Z)
• Can LLMs Separate Instructions From Data? And What Do We Even Mean By That? [60.50127555651554]
  大規模言語モデル(LLM)は、多くの実用的なアプリケーションにおいて印象的な結果を示すが、基本的な安全性機能は欠如している。 これにより、間接的なプロンプトインジェクションのような操作に脆弱になり、一般に安全クリティカルなタスクには適さない。 モデル出力から計算可能な命令データ分離の形式的尺度と経験的変量を導入する。
  論文  参考訳（メタデータ） (2024-03-11T15:48:56Z)
• GPU-Accelerated Verification of Machine Learning Models for Power Systems [0.0]
  近年,大規模機械学習(ML)モデルの性能を厳格に検証するための計算ツールが著しく進歩している。 しかし、彼らの成功にもかかわらず、これらのルーチンがシステム問題へのアウト・オブ・ボックス適用を妨げている。 本稿では,この問題を2つの重要な方法で解決する。 私たちは、$alpha,beta$-CROWNソルバを使って、最初の一連のイノベーションを構築し、テストします。
  論文  参考訳（メタデータ） (2023-06-18T18:46:16Z)
• Machine Learning with Requirements: a Manifesto [114.97965827971132]
  要件定義と満足度は、マシンラーニングモデルが現実世界にさらに適合するように、長い道のりを歩むことができる、と私たちは主張しています。 私たちは、要求仕様を標準の機械学習開発パイプラインにうまく組み込む方法を示します。
  論文  参考訳（メタデータ） (2023-04-07T14:47:13Z)
• On a Uniform Causality Model for Industrial Automation [61.303828551910634]
  産業自動化の様々な応用分野に対する一様因果モデルを提案する。 得られたモデルは、サイバー物理システムの振る舞いを数学的に記述する。 このモデルは、機械学習に焦点を当てた産業自動化における新しいアプローチの応用の基盤として機能することが示されている。
  論文  参考訳（メタデータ） (2022-09-20T11:23:51Z)
• Ising machines as hardware solvers of combinatorial optimization problems [1.8732539895890135]
  イジングマシンは、アイジングモデルの絶対的あるいは近似的な基底状態を見つけることを目的としたハードウェアソルバである。 既存の標準デジタルコンピュータより優れたスケーラブルなIsingマシンは、実用アプリケーションに大きな影響を与える可能性がある。
  論文  参考訳（メタデータ） (2022-04-01T08:24:06Z)
• SOLIS -- The MLOps journey from data acquisition to actionable insights [62.997667081978825]
  本稿では,基本的なクロスプラットフォームテンソルフレームワークとスクリプト言語エンジンを使用しながら,すべての要件をサポートする統合デプロイメントパイプラインとフリー・ツー・オペレートアプローチを提案する。 しかし、このアプローチは、実際のプロダクショングレードシステムに機械学習機能を実際にデプロイするために必要な手順やパイプラインを提供していない。
  論文  参考訳（メタデータ） (2021-12-22T14:45:37Z)
• Efficient time stepping for numerical integration using reinforcement learning [0.15393457051344295]
  機械学習とメタラーニングに基づくデータ駆動型タイムステッピング方式を提案する。 まず、1つまたは複数の基礎学習者(非滑らかまたはハイブリッドシステムの場合)はRLを使用して訓練されます。 次に、メタ学習者は(システムの状態に応じて)現在の状況に最適と思われる基礎学習者を選択する訓練を受ける。
  論文  参考訳（メタデータ） (2021-04-08T07:24:54Z)
• Probably Approximately Correct Constrained Learning [135.48447120228658]
  我々は、ほぼ正しい学習フレームワーク(PAC)に基づく一般化理論を開発する。 PAC学習可能なクラスも制約のある学習者であるという意味では,学習者の導入は学習問題を難しくするものではないことを示す。 このソリューションの特性を分析し,制約付き学習が公平でロバストな分類における問題にどのように対処できるかを説明する。
  論文  参考訳（メタデータ） (2020-06-09T19:59:29Z)

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

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